diff options
Diffstat (limited to 'contrib/funind/tacinvutils.ml')
| -rw-r--r-- | contrib/funind/tacinvutils.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index a125b9a7..2877c19d 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -21,9 +21,9 @@ open Reductionops (*s printing of constr -- debugging *) (* comment this line to see debug msgs *) -let msg x = () ;; let prterm c = str "" +let msg x = () ;; let pr_lconstr c = str "" (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ prterm c ++ str"\n") +let prconstr c = msg (str" " ++ pr_lconstr c ++ str"\n") let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) @@ -31,7 +31,7 @@ let prchr () = msg (str" (ret) \n") let prNamedConstr s c = begin msg(str ""); - msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n"); + msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n"); msg(str ""); end @@ -74,7 +74,7 @@ let rec mkevarmap_from_listex lex = let _ = prconstr typ in*) let info ={ evar_concl = typ; - evar_hyps = empty_named_context; + evar_hyps = empty_named_context_val; evar_body = Evar_empty} in Evd.add (mkevarmap_from_listex lex') ex info @@ -126,7 +126,7 @@ let apply_leqtrpl_t t leq = let apply_refl_term eq t = - let _,arr = destApplication eq in + let _,arr = destApp eq in let reli= (Array.get arr 1) in let by_t= (Array.get arr 2) in substitterm 0 reli by_t t @@ -144,7 +144,7 @@ let apply_eq_leqtrpl leq eq = let constr_head_match u t= if isApp u then - let uhd,args= destApplication u in + let uhd,args= destApp u in uhd=t else false @@ -187,7 +187,7 @@ let rec buildrefl_from_eqs eqs = match eqs with | [] -> [] | cstr::eqs' -> - let eq,args = destApplication cstr in + let eq,args = destApp cstr in (mkRefl (Array.get args 0) (Array.get args 2)) :: (buildrefl_from_eqs eqs') @@ -237,7 +237,7 @@ let rec substit_red prof t by_t in_u = (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each reli by tarr.(f-i). *) let exchange_reli_arrayi tarr (d,f) t = - let hd,args= destApplication t in + let hd,args= destApp t in let i = destRel hd in let res = whd_beta (mkApp (tarr.(f-i) ,args)) in res @@ -269,7 +269,7 @@ let def_of_const t = (* nom d'une constante. Must be a constante. x*) let name_of_const t = match (kind_of_term t) with - Const cst -> Names.string_of_label (Names.label cst) + Const cst -> Names.string_of_label (Names.con_label cst) |_ -> assert false ;; |