aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-12-07 12:28:14 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-12-07 12:28:14 +0100
commitad768e435a736ca51ac79a575967b388b34918c7 (patch)
tree6f87c9bc585d15862b66c39feb3a5172e468f67f /plugins
parentcf8ecf83b5cc52f7ea73dc1d3af59bf03deff688 (diff)
parent40cffd816b7adbf8f136f62f6f891fb5be9b96a6 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/g_ground.ml46
-rw-r--r--plugins/ssrmatching/ssrmatching.ml49
2 files changed, 10 insertions, 5 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 344a04a6a..260e86ad6 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -116,9 +116,9 @@ open Pp
open Genarg
open Ppconstr
open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
let warn_deprecated_syntax =
CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a688fc065..0d4be72d9 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -435,7 +435,7 @@ let proj_nparams c =
try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
let isFixed c = match kind_of_term c with
- | Var _ | Ind _ | Construct _ | Const _ -> true
+ | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
| _ -> false
let isRigid c = match kind_of_term c with
@@ -487,6 +487,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
let np = proj_nparams p in
if np = 0 || np > List.length a then KpatConst, f, a else
let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2
+ | Proj (p,arg) -> KpatProj (Projection.constant p), f, a
| Var _ | Ind _ | Construct _ -> KpatFixed, f, a
| Evar (k, _) ->
if Evd.mem sigma0 k then KpatEvar k, f, a else
@@ -567,6 +568,10 @@ let filter_upat i0 f n u fpats =
if np < na then fpats else
let () = if !i0 < np then i0 := n in (u, np) :: fpats
+let eq_prim_proj c t = match kind_of_term t with
+ | Proj(p,_) -> Constant.equal (Projection.constant p) c
+ | _ -> false
+
let filter_upat_FO i0 f n u fpats =
let np = nb_args u.up_FO in
if n < np then fpats else
@@ -577,7 +582,7 @@ let filter_upat_FO i0 f n u fpats =
| KpatLet -> isLetIn f
| KpatLam -> isLambda f
| KpatRigid -> isRigid f
- | KpatProj pc -> Term.eq_constr f (mkConst pc)
+ | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f
| KpatFlex -> i0 := n; true in
if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats