Experimental commit: definitions are now allowed in contexts. As a consequence,

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 7781be6ae11e7fc1187b0c13dcad398d13a88d3e..5457708a0a41a143d8ccd2824b931a2cdb97ed1f 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -162,6 +162,15 @@ let perforate context term ty =
 
 exception Fail of string;;
 
+(*CSC: generatore di nomi? Chiedere il nome? *)
+let fresh_name =
+ let next_fresh_index = ref 0
+in
+ function () ->
+  incr next_fresh_index ;
+  "fresh_name" ^ string_of_int !next_fresh_index
+;;
+
 (* lambda_abstract newmeta ty *)
 (* returns a triple [bo],[context],[ty'] where              *)
 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
@@ -179,7 +188,7 @@ let lambda_abstract newmeta ty =
          match n with
             C.Name _ -> n
 (*CSC: generatore di nomi? Chiedere il nome? *)
-          | C.Anonimous -> C.Name "fresh_name"
+          | C.Anonimous -> C.Name (fresh_name ())
         in
          ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
     | C.LetIn (n,s,t) ->
@@ -229,7 +238,7 @@ let exact bo =
        metano,context,ty
   in
    let context = cic_context_of_named_context context in
-    if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
+    if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then
      begin
       refine_meta metano bo [] ;
       goal := None
@@ -577,7 +586,8 @@ let reduction_tactic reduction_function term =
      None -> assert false
    | Some (metano,(context,ty)) -> metano,context,ty
  in
-  let term' = reduction_function term in
+  let ciccontext = cic_context_of_named_context context in
+  let term' = reduction_function ciccontext term in
    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
    (* the type of one metavariable. So we replace it everywhere.   *)
    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
@@ -613,7 +623,8 @@ let reduction_tactic_in_scratch reduction_function ty term =
      None -> []
    | Some (_,(context,_)) -> context
  in
-  let term' = reduction_function term in
+  let ciccontext = cic_context_of_named_context context in
+  let term' = reduction_function ciccontext term in
    ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
 ;;
 
@@ -639,7 +650,8 @@ let fold term =
      None -> assert false
    | Some (metano,(context,ty)) -> metano,context,ty
  in
-  let term' = CicReduction.whd term in
+  let ciccontext = cic_context_of_named_context context in
+  let term' = CicReduction.whd ciccontext term in
    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
    (* the type of one metavariable. So we replace it everywhere.   *)
    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
@@ -736,7 +748,7 @@ let change ~goal_input ~input =
   let ciccontext = cic_context_of_named_context context in
    (* are_convertible works only on well-typed terms *)
    ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
-   if CicReduction.are_convertible goal_input input then
+   if CicReduction.are_convertible ciccontext goal_input input then
     begin
      let ty' = ProofEngineReduction.replace goal_input input ty in
       let metasenv' =