diff options
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r-- | pretyping/detyping.ml | 46 |
1 files changed, 24 insertions, 22 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bb563220b..df89d9eac 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -14,6 +14,7 @@ open Pp open CErrors open Util open Names +open Constr open Term open EConstr open Vars @@ -26,7 +27,6 @@ open Libnames open Globnames open Nametab open Mod_subst -open Misctypes open Decl_kinds open Context.Named.Declaration open Ltac_pretype @@ -36,7 +36,7 @@ type _ delay = | Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) -let print_universes = Flags.univ_print +let print_universes = ref false (** If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false @@ -920,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -929,9 +929,11 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make () let rec subst_glob_constr subst = DAst.map (function | GRef (ref,u) as raw -> - let ref',t = subst_global subst ref in - if ref' == ref then raw else - DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t)) + let ref',t = subst_global subst ref in + if ref' == ref then raw else + let env = Global.env () in + let evd = Evd.from_env env in + DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)) | GSort _ | GVar _ @@ -940,7 +942,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -957,25 +959,25 @@ let rec subst_glob_constr subst = DAst.map (function | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in - let t' = Option.smartmap (subst_glob_constr subst) t in + let t' = Option.Smart.map (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in - let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + let rtno' = Option.Smart.map (subst_glob_constr subst) rtno + and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in - let topt' = Option.smartmap + let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -985,14 +987,14 @@ let rec subst_glob_constr subst = DAst.map (function GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 and c' = subst_glob_constr subst c in @@ -1000,12 +1002,12 @@ let rec subst_glob_constr subst = DAst.map (function GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> - let ra1' = Array.smartmap (subst_glob_constr subst) ra1 - and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in - let bl' = Array.smartmap - (List.smartmap (fun (na,k,obd,ty as dcl) -> + let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 + and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in + let bl' = Array.Smart.map + (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in - let obd' = Option.smartmap (subst_glob_constr subst) obd in + let obd' = Option.Smart.map (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else @@ -1018,13 +1020,13 @@ let rec subst_glob_constr subst = DAst.map (function if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in + let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in - let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in + let k' = smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') | GProj (p,c) as raw -> |