- removed some unneeded dependencies from debian/control

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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index b1aa1a256f707a11f8aff9b76a9de7f922873747..537ef3f5d986f06286ca7ea341cb9d2c750bed0f 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -737,9 +737,9 @@ let r =
 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-  let fresh_meta = ProofEngineHelpers.new_meta proof in
+  let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
-   ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+   CicMkImplicit.identity_relocation_list_for_metavariable context in
   let metasenv' = (fresh_meta,context,t)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
@@ -762,9 +762,9 @@ let my_cut ~term:c ~status:(proof,goal)=
 debug("my_cut di "^CicPp.ppterm c^"\n");
 
 
-  let fresh_meta = ProofEngineHelpers.new_meta proof in
+  let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
-   ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+   CicMkImplicit.identity_relocation_list_for_metavariable context in
   let metasenv' = (fresh_meta,context,c)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
@@ -886,8 +886,10 @@ let rec superlift c n=
   [] -> []
   | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(
                   CicSubstitution.lift n a))] @ superlift next (n+1)
-  | Some(name,Cic.Def(a))::next   -> [Some(name,Cic.Def(
-                  CicSubstitution.lift n a))] @ superlift next (n+1)
+  | Some(name,Cic.Def(a,None))::next   -> [Some(name,Cic.Def((
+                  CicSubstitution.lift n a),None))] @ superlift next (n+1)
+  | Some(name,Cic.Def(a,Some ty))::next   -> [Some(name,Cic.Def((
+                  CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1)
   | _::next -> superlift next (n+1) (*??  ??*)
  
 ;;
@@ -899,9 +901,9 @@ debug("inizio EQ\n");
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
-   let fresh_meta = ProofEngineHelpers.new_meta proof in
+   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
    let irl =
-    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+    CicMkImplicit.identity_relocation_list_for_metavariable context in
    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
    let (proof,goals) =