parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / fourierR.ml

diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml
index 8e443447a892f2a160fd7c724697698857a987b8..eb3201c58587b051170991690254d29a17434148 100644 (file)
--- a/helm/software/components/tactics/fourierR.ml
+++ b/helm/software/components/tactics/fourierR.ml
@@ -439,8 +439,8 @@ let fourier_lineq lineq1 =
    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
    List.iter (fun f ->
                Hashtbl.iter (fun x c ->
-                                 try (Hashtbl.find hvar x;())
-                                 with _-> nvar:=(!nvar)+1;
+                                 try ignore(Hashtbl.find hvar x)
+                                 with Not_found -> nvar:=(!nvar)+1;
                                              Hashtbl.add hvar x (!nvar);
                                           debug("aggiungo una var "^
                                            string_of_int !nvar^" per "^
@@ -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) (*??  ??*)