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 /printing/printmod.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 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 3438063f76..f4986652b3 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -10,6 +10,7 @@ open Util open Constr +open Context open Pp open Names open Environ @@ -132,10 +133,10 @@ let get_fields = let rec prodec_rec l subst c = match kind c with | Prod (na,t,c) -> - let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in + let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c | LetIn (na,b,_,c) -> - let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in + let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c | _ -> List.rev l in |