Signature and concrete syntax of fold fixed.

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 728ff94a085157d37933e1d14e782f108c2866d6..e59e139872e252751a2168e5f58aabc866374a68 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -398,8 +398,8 @@ EXTEND
     | IDENT "exists" ->
         TacticAst.Exists loc
     | IDENT "fail" -> TacticAst.Fail loc
-    | IDENT "fold"; kind = reduction_kind; p = pattern_spec ->
-        TacticAst.Fold (loc, kind, p)
+    | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
+        TacticAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         TacticAst.Fourier loc
     | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 3f6e74346ec04e98e1bedb0da085dffd7442fb1e..c4f2a29ac4a389cc7ff9ac7e128fb8ea0e2b1efb 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -50,7 +50,7 @@ type ('term, 'ident) tactic =
   | Exact of loc * 'term
   | Exists of loc
   | Fail of loc
-  | Fold of loc * reduction_kind * ('term, 'ident) pattern
+  | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
   | Fourier of loc
   | FwdSimpl of loc * string * 'ident list
   | Generalize of loc * ('term, 'ident) pattern * 'ident option

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 67b5733d2a0644ef7376a6eff154af6810af2942..86c7185ecf1308d75e1f34707059c1cc77f3fc1f 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -82,8 +82,9 @@ let rec pp_tactic = function
   | ElimType (_, term) -> "elim type " ^ pp_term_ast term
   | Exact (_, term) -> "exact " ^ pp_term_ast term
   | Exists _ -> "exists"
-  | Fold (_, kind, pattern) ->
-      sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern)
+  | Fold (_, kind, term, pattern) ->
+      sprintf "fold %s %s %s" (pp_reduction_kind kind)
+       (pp_term_ast term) (pp_pattern pattern)
   | FwdSimpl (_, hyp, idents) -> 
       sprintf "fwd %s%s" hyp 
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 2fbba97ad5b7d905d48b8ddde2c96bf40a252136..3079b327b09ee47179f0468eb259074932810fd1 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -693,16 +693,12 @@ let tac_zero_infeq_false gl (n,d) =
    (Tacticals.then_
     ~start:
       (ReductionTactics.fold_tac ~reduction:CicReduction.whd
-        ~pattern:
-          (ProofEngineTypes.conclusion_pattern
-            (Some
-              (Cic.Appl
-                [_Rle ; _R0 ;
-                 Cic.Appl
-                  [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
-                ]
-              )))
-      )
+        ~pattern:(ProofEngineTypes.conclusion_pattern None)
+        ~term:
+          (Cic.Appl
+            [_Rle ; _R0 ;
+              Cic.Appl
+               [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]]))
     ~continuation:
       (Tacticals.then_ 
         ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index ae99ecb33d486be1f0069a9fce4b46f076b3a5f5..18db1a302dab0a3cbec4849e32202ca0bc137b27 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -83,7 +83,7 @@ let whd_tac ~pattern =
 let normalize_tac ~pattern = 
  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
 
-let fold_tac ~reduction ~pattern =
+let fold_tac ~reduction ~term ~pattern =
 (*
  let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal)
  =

diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli
index 20e45827d2de436954314279261fdb397728d1e4..00d3e58900b2789f6ce895d826cffd57553cd00f 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.mli
+++ b/helm/ocaml/tactics/reductionTactics.mli
@@ -30,5 +30,5 @@ val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 
 val fold_tac:
- reduction:(Cic.context -> Cic.term -> Cic.term) ->
+ reduction:(Cic.context -> Cic.term -> Cic.term) -> term:Cic.term ->
  pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 187dc2be3b4725e70cf9b8f376ea90bbb562533a..c155d67d39adecb386a861e47bdec3f01f4f492e 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -33,6 +33,7 @@ val exists : ProofEngineTypes.tactic
 val fail : ProofEngineTypes.tactic
 val fold :
   reduction:(Cic.context -> Cic.term -> Cic.term) ->
+  term:Cic.term ->
   pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val fourier : ProofEngineTypes.tactic
 val fwd_simpl :