Defs in context may now have an optional type (when unknown).

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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index b1aa1a256f707a11f8aff9b76a9de7f922873747..a807554c5be305e8f7d4285f23d3f11fcf9195f0 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -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) (*??  ??*)
  
 ;;