first moogle template checkin

[helm.git] / helm / ocaml / tactics / reductionTactics.ml

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index b29873a1fceae31c4521c231bfd503ce29b65585..80cb3306a18b79a4c08e1c8b40e9625014f86c9e 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -24,9 +24,9 @@
  *)
 
 (*
-let reduction_tac ~reduction ~status:(proof,goal) =
+let reduction_tac ~reduction (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let new_ty = reduction context ty in
    let new_metasenv = 
     List.map
@@ -40,9 +40,9 @@ let reduction_tac ~reduction ~status:(proof,goal) =
 *)
 
 (* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
+let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let terms =
    match terms with None -> [ty] | Some l -> l
   in
@@ -69,11 +69,12 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
       List.fold_right
        (fun entry context ->
          match entry with
-            Some (name,Cic.Def  t) ->
-             (Some (name,Cic.Def  (replace context t)))::context
+            Some (name,Cic.Def (t,None)) ->
+             (Some (name,Cic.Def ((replace context t),None)))::context
           | Some (name,Cic.Decl t) ->
              (Some (name,Cic.Decl (replace context t)))::context
           | None -> None::context
+          | Some (_,Cic.Def (_,Some _)) -> assert false
        ) context []
      else
       context
@@ -92,9 +93,9 @@ let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
 let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
 let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
 
-let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
+let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let term' = reduction context 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.   *)
@@ -110,8 +111,9 @@ let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
        List.map
         (function
             Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
-          | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
+          | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
           | None -> None
+          | Some (_,Cic.Def (_,Some _)) -> assert false
         ) context
       else
        context