diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 9258a39fc..1795336f4 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -53,7 +53,7 @@ let subst_evar_in_evm evar def evm = let rec safe_define evm ev c = if not (closedn (-1) c) then raise Termops.CannotFilter else -(* msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) +(* msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Pp.int ev++str" := "++pr_constr c);*) let evi = (Evd.find evm ev) in let define_subst evm sigma = Util.Intmap.fold @@ -99,7 +99,7 @@ module SubstSet : Set.S with type elt = Termops.subst let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = let ev_typ = Libtypes.reduce (evar_concl evi) in let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in -(* msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*) +(* msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Pp.int ev);*) let substs = ref SubstSet.empty in try List.iter ( fun (gr,(pat,_),s) -> @@ -107,7 +107,7 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = let genl = List.map (fun (_,_,t) -> t) genl in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in let def = applistc (Libnames.constr_of_global gr) argl in -(* msgnl(str"essayons ?"++Util.pr_int ev++spc()++str":="++spc() +(* msgnl(str"essayons ?"++Pp.int ev++spc()++str":="++spc() ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*) (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*) try @@ -145,7 +145,7 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit let tyl = List.map (fun (_,_,t) -> t) ctx in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in let def = applistc c argl in -(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) +(* msgnl(str"trouvé def ?"++Pp.int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) try if not (Evd.is_defined evm ev) then let evm = safe_define evm ev def in @@ -222,7 +222,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature ( fun ctx typ -> List.iter (fun ((cl,ev,evm),_,_) -> -(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*) +(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Pp.int ev++str " dans "++pr_evar_map evm);*) smap := Gmapl.add (cl,evm) (ctx,ev) !smap) (Recordops.methods_matching typ) ) [] deftyp; @@ -265,7 +265,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit) then Evd.remove evm ev,gen else evm,(ev::gen)) gen (evm,[]) in -(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*) +(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Pp.int gen++str"] : "++spc()++pr_evar_map evm);*) let ngen = List.length gen in let (_,ctx,evm) = List.fold_left ( fun (i,ctx,evm) ev -> |