* Many improvements

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 60baf8e59e4bce3f4697c21c3199d979c9852793..90d18998111695f18578ddc6ae031f27c89876e0 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -539,6 +539,11 @@ prerr_endline "dopo refine meta" ; flush stdout ;
                  | [] -> goal := None
 ;;
 
+let elim_intros term =
+ elim term ;
+ intros ()
+;;
+
 let reduction_tactic reduction_function term =
  let curi,metasenv,pbo,pty =
   match !proof with
@@ -551,47 +556,27 @@ let reduction_tactic reduction_function term =
    | Some (metano,(context,ty)) -> metano,context,ty
  in
   let term' = reduction_function term in
-   let ty' = ProofEngineReduction.replace term term' ty in
-    let metasenv' = 
-     List.map
-      (function
-          (n,_) when n = metano -> (metano,ty')
-        | _ as t -> t
-      ) metasenv
-    in
-     proof := Some (curi,metasenv',pbo,pty) ;
-     goal := Some (metano,(context,ty'))
+   (* 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 *)
+   (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
+   let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
+    let ty' = replace ty in
+    let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_) when n = metano -> (metano,ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      proof := Some (curi,metasenv',pbo,pty) ;
+      goal := Some (metano,(context',ty'))
 ;;
 
 let whd    = reduction_tactic CicReduction.whd;;
 let reduce = reduction_tactic ProofEngineReduction.reduce;;
-(*
 let simpl  = reduction_tactic ProofEngineReduction.simpl;;
-*)
-
-let simpl term =
- let curi,metasenv,pbo,pty =
-  match !proof with
-     None -> assert false
-   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let (metano,context,ty) =
-  match !goal with
-     None -> assert false
-   | Some (metano,(context,ty)) -> metano,context,ty
- in
-  let term' = ProofEngineReduction.simpl term in
-   let ty' = ProofEngineReduction.replace term term' ty in
-    let metasenv' = 
-     List.map
-      (function
-          (n,_) when n = metano -> (metano,ty')
-        | _ as t -> t
-      ) metasenv
-    in
-     proof := Some (curi,metasenv',pbo,pty) ;
-     goal := Some (metano,(context,ty'))
-;;
 
 (* It is just the opposite of whd. The code should probably be merged. *)
 let fold term =
@@ -606,16 +591,22 @@ let fold term =
    | Some (metano,(context,ty)) -> metano,context,ty
  in
   let term' = CicReduction.whd term in
-   let ty' = ProofEngineReduction.replace term' term ty in
-    let metasenv' = 
-     List.map
-      (function
-          (n,_) when n = metano -> (metano,ty')
-        | _ as t -> t
-      ) metasenv
-    in
-     proof := Some (curi,metasenv',pbo,pty) ;
-     goal := Some (metano,(context,ty'))
+   (* 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 *)
+   (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
+   let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
+    let ty' = replace ty in
+    let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_) when n = metano -> (metano,ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      proof := Some (curi,metasenv',pbo,pty) ;
+      goal := Some (metano,(context',ty'))
 ;;
 
 let cut term =