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 /plugins/ssrmatching | |
| 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 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index fb99b87108..b83a6a34cb 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -16,6 +16,7 @@ open Pp open Genarg open Stdarg open Term +open Context module CoqConstr = Constr open CoqConstr open Vars @@ -383,7 +384,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = | Context.Named.Declaration.LocalDef (x, b, t) -> d, mkNamedLetIn x (put b) (put t) c | Context.Named.Declaration.LocalAssum (x, t) -> - mkVar x :: d, mkNamedProd x (put t) c in + mkVar x.binder_name :: d, mkNamedProd x (put t) c in let a, t = Context.Named.fold_inside abs_dc ~init:([], (put @@ EConstr.Unsafe.to_constr evi.evar_concl)) @@ -548,7 +549,7 @@ let match_upats_FO upats env sigma0 ise orig_c = if skip || not (closed0 c') then () else try let _ = match u.up_k with | KpatFlex -> - let kludge v = mkLambda (Anonymous, mkProp, v) in + let kludge v = mkLambda (make_annot Anonymous Sorts.Relevant, mkProp, v) in unif_FO env ise (kludge u.up_FO) (kludge c') | KpatLet -> let kludge vla = @@ -1286,7 +1287,7 @@ let ssrpatterntac _ist arg gl = let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in - let concl = EConstr.mkLetIn (Name (Id.of_string "selected"), t, tty, concl_x) in + let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) |