diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /proofs/clenv.ml | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9540d3de44..2d2113b636 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -15,6 +15,7 @@ open Names open Nameops open Termops open Constr +open Context open Namegen open Environ open Evd @@ -69,7 +70,7 @@ let clenv_push_prod cl = | Prod (na,t,u) -> let mv = new_meta () in let dep = not (noccurn (cl_sigma cl) 1 u) in - let na' = if dep then na else Anonymous in + let na' = if dep then na.binder_name else Anonymous in let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in let def = applist (cl.templval.rebus,[mkMeta mv]) in @@ -103,7 +104,7 @@ let clenv_environments evd bound t = | (n, Prod (na,t1,t2)) -> let mv = new_meta () in let dep = not (noccurn evd 1 t2) in - let na' = if dep then na else Anonymous in + let na' = if dep then na.binder_name else Anonymous in let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) @@ -277,7 +278,7 @@ let adjust_meta_source evd mv = function | loc,Evar_kinds.VarInstance id -> let rec match_name c l = match EConstr.kind evd c, l with - | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id + | Lambda ({binder_name=Name id},_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id | Lambda (_,_,c), a::l -> match_name c l | _ -> None in (* This is very ad hoc code so that an evar inherits the name of the binder @@ -623,7 +624,7 @@ let make_evar_clause env sigma ?len t = hole_type = t1; hole_deps = dep; (* We fix it later *) - hole_name = na; + hole_name = na.binder_name; } in let t2 = if dep then subst1 ev t2 else t2 in clrec (sigma, hole :: holes) inst (pred n) t2 |