X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FfourierR.ml;h=4844978030fab7c3f78a90060965491cd1e13d51;hb=f2e2d1f6cccad2cc1ce70ef7fa2841cf0a457953;hp=8e443447a892f2a160fd7c724697698857a987b8;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml
index 8e443447a..484497803 100644
--- a/helm/software/components/tactics/fourierR.ml
+++ b/helm/software/components/tactics/fourierR.ml
@@ -858,11 +858,9 @@ 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,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(a,ty))::next   -> 
      [Some(name,
-      Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))
+      Cic.Def((CicSubstitution.lift n a),CicSubstitution.lift n ty))
       ] @ superlift next (n+1)
   | _::next -> superlift next (n+1) (*??  ??*)