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 "^
[] -> []
| 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) (*?? ??*)