diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 63 |
1 files changed, 31 insertions, 32 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 87d3880f99..eaa5736336 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -145,9 +145,9 @@ let add_name_opt na b t (nenv, env) = (****************************************************************************) (* Tools for printing of Cases *) -let encode_inductive r = +let encode_inductive env r = let indsp = Nametab.global_inductive r in - let constr_lengths = constructors_nrealargs indsp in + let constr_lengths = constructors_nrealargs env indsp in (indsp,constr_lengths) (* Parameterization of the translation from constr to ast *) @@ -159,15 +159,15 @@ let has_two_constructors lc = let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1 -let encode_bool ({CAst.loc} as r) = - let (x,lc) = encode_inductive r in +let encode_bool env ({CAst.loc} as r) = + let (x,lc) = encode_inductive env r in if not (has_two_constructors lc) then user_err ?loc ~hdr:"encode_if" (str "This type has not exactly two constructors."); x -let encode_tuple ({CAst.loc} as r) = - let (x,lc) = encode_inductive r in +let encode_tuple env ({CAst.loc} as r) = + let (x,lc) = encode_inductive env r in if not (isomorphic_to_tuple lc) then user_err ?loc ~hdr:"encode_tuple" (str "This type cannot be seen as a tuple type."); @@ -175,7 +175,7 @@ let encode_tuple ({CAst.loc} as r) = module PrintingInductiveMake = functor (Test : sig - val encode : qualid -> inductive + val encode : Environ.env -> qualid -> inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -1014,13 +1014,12 @@ let rec subst_cases_pattern subst = DAst.map (function let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst = DAst.map (function +let rec subst_glob_constr env subst = DAst.map (function | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else (match t with | None -> GRef (ref', u) | Some t -> - let env = Global.env () in let evd = Evd.from_env env in let t = t.Univ.univ_abstracted_value in (* XXX This seems dangerous *) DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))) @@ -1032,33 +1031,33 @@ let rec subst_glob_constr subst = DAst.map (function | GPatVar _ as raw -> raw | GApp (r,rl) as raw -> - let r' = subst_glob_constr subst r - and rl' = List.Smart.map (subst_glob_constr subst) rl in + let r' = subst_glob_constr env subst r + and rl' = List.Smart.map (subst_glob_constr env subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') | GLambda (n,bk,r1,r2) as raw -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in + let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in if r1' == r1 && r2' == r2 then raw else GLambda (n,bk,r1',r2') | GProd (n,bk,r1,r2) as raw -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in + let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in if r1' == r1 && r2' == r2 then raw else GProd (n,bk,r1',r2') | 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.Smart.map (subst_glob_constr subst) t in + let r1' = subst_glob_constr env subst r1 in + let r2' = subst_glob_constr env subst r2 in + let t' = Option.Smart.map (subst_glob_constr env 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.Smart.map (subst_glob_constr subst) rtno + let rtno' = Option.Smart.map (subst_glob_constr env subst) rtno and rl' = List.Smart.map (fun (a,x as y) -> - let a' = subst_glob_constr subst a in + let a' = subst_glob_constr env subst a in let (n,topt) = x in let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> @@ -1069,7 +1068,7 @@ let rec subst_glob_constr subst = DAst.map (function (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = List.Smart.map (subst_cases_pattern subst) cpl - and r' = subst_glob_constr subst r in + and r' = subst_glob_constr env subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) branches @@ -1078,27 +1077,27 @@ 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.Smart.map (subst_glob_constr subst) po - and b' = subst_glob_constr subst b - and c' = subst_glob_constr subst c in + let po' = Option.Smart.map (subst_glob_constr env subst) po + and b' = subst_glob_constr env subst b + and c' = subst_glob_constr env 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.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 + let po' = Option.Smart.map (subst_glob_constr env subst) po + and b1' = subst_glob_constr env subst b1 + and b2' = subst_glob_constr env subst b2 + and c' = subst_glob_constr env subst c in if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> - let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 - and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in + let ra1' = Array.Smart.map (subst_glob_constr env subst) ra1 + and ra2' = Array.Smart.map (subst_glob_constr env 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.Smart.map (subst_glob_constr subst) obd in + let ty' = subst_glob_constr env subst ty in + let obd' = Option.Smart.map (subst_glob_constr env 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 @@ -1116,8 +1115,8 @@ let rec subst_glob_constr subst = DAst.map (function else GHole (nknd, naming, nsolve) | GCast (r1,k) as raw -> - let r1' = subst_glob_constr subst r1 in - let k' = smartmap_cast_type (subst_glob_constr subst) k in + let r1' = subst_glob_constr env subst r1 in + let k' = smartmap_cast_type (subst_glob_constr env subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') ) |