The user interface for the completeSearchPattern query has been improved.

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index dbf04c393386c0d57e5e74faf57ec4e9b242092f..73e2aa177dfa76a0d8280b8f0813bf4f52e3d602 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -138,11 +138,10 @@ let perforate context term ty =
 
 (*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
+ let next_fresh_index = ref 0 in
+  function () ->
+   incr next_fresh_index ;
+   "fresh_name" ^ string_of_int !next_fresh_index
 
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 let reduction_tactic_in_scratch reduction_function term ty =
@@ -174,7 +173,7 @@ let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 let intros () =
-  apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
+  apply_tactic (PrimitiveTactics.intros_tac ~mknames:fresh_name)
 let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
 let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
@@ -200,8 +199,18 @@ let simpl term =
  apply_tactic
   (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some term))
 
-let fold term =
- apply_tactic (ReductionTactics.fold_tac ~also_in_hypotheses:true ~term)
+let fold_whd term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+    ~also_in_hypotheses:true ~term)
+let fold_reduce term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce
+    ~also_in_hypotheses:true ~term)
+let fold_simpl term =
+ apply_tactic
+  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl
+    ~also_in_hypotheses:true ~term)
 
   (* other tactics *)