X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=a807554c5be305e8f7d4285f23d3f11fcf9195f0;hb=e7e2a523299d807370b292b44e77f46fad1638c9;hp=b1aa1a256f707a11f8aff9b76a9de7f922873747;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index b1aa1a256..a807554c5 100644
--- 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) (*??  ??*)
  
 ;;