aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--README.ci.md (renamed from README.ci)10
-rwxr-xr-xdev/ci/ci-fiat-parsers.sh2
-rw-r--r--dev/ci/ci-user-overlay.sh8
-rw-r--r--interp/constrextern.ml10
-rw-r--r--interp/constrintern.ml16
-rw-r--r--interp/constrintern.mli2
-rw-r--r--intf/evar_kinds.mli5
-rw-r--r--intf/glob_term.mli2
-rw-r--r--plugins/funind/g_indfun.ml426
-rw-r--r--plugins/funind/glob_term_to_relation.ml13
-rw-r--r--plugins/funind/glob_termops.ml45
-rw-r--r--plugins/funind/glob_termops.mli7
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/invfun.ml25
-rw-r--r--plugins/ltac/pptactic.ml54
-rw-r--r--plugins/ltac/pptactic.mli4
-rw-r--r--plugins/ltac/tacintern.ml4
-rw-r--r--plugins/ltac/tacinterp.ml4
-rw-r--r--pretyping/glob_ops.ml9
-rw-r--r--pretyping/patternops.ml11
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--printing/miscprint.ml25
-rw-r--r--printing/miscprint.mli13
-rw-r--r--stm/stm.ml6
-rw-r--r--tactics/hipattern.ml2
25 files changed, 158 insertions, 151 deletions
diff --git a/README.ci b/README.ci.md
index 43e1bd740..9e25390d7 100644
--- a/README.ci
+++ b/README.ci.md
@@ -24,11 +24,11 @@ the latest Coq changes validated against your development?
If so, keep reading! Getting Coq changes tested against your library
is easy, all that you need to do is:
-1.- Put you development in a public repository tracking coq trunk.
-2.- Make sure that your development builds in less than 35 minutes.
-3.- Submit a PR adding your development.
-4.- ?
-5.- Profit! Your library is now part of Coq's continous integration!
+1. Put you development in a public repository tracking coq trunk.
+2. Make sure that your development builds in less than 35 minutes.
+3. Submit a PR adding your development.
+4. ?
+5. Profit! Your library is now part of Coq's continous integration!
Note that by partipating in this program, you assume a reasonable
compromise to discuss and eventually integrate compatibility changes
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index c62aa1d85..a0cb008a3 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
-( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers && make -j ${NJOBS} fiat-core )
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index bfa43cde1..398c12707 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,10 +25,8 @@ echo $TRAVIS_PULL_REQUEST
echo $TRAVIS_BRANCH
echo $TRAVIS_COMMIT
-if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then
-
- mathcomp_CI_BRANCH=coqlib-part-02
- mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
-
+if [ $TRAVIS_PULL_REQUEST == "590" ] || [ $TRAVIS_BRANCH == "trunk+algebraic-matchingvar" ]; then
+ mathcomp_CI_BRANCH=trunk+pr590-patvar
+ mathcomp_CI_GITURL=https://github.com/herbelin/math-comp.git
fi
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5dc02e602..19ca8d50b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -663,9 +663,11 @@ let rec extern inctx scopes vars r =
| GEvar (n,l) ->
extern_evar n (List.map (on_snd (extern false scopes vars)) l)
- | GPatVar (b,n) ->
+ | GPatVar kind ->
if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
- if b then CPatVar n else CEvar (n,[])
+ (match kind with
+ | Evar_kinds.SecondOrderPatVar n -> CPatVar n
+ | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
| GApp (f,args) ->
(match f with
@@ -1037,13 +1039,13 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
GVar id
| PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
- | PMeta (Some n) -> GPatVar (false,n)
+ | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
| PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None),
[glob_of_pat env sigma c])
| PApp (f,args) ->
GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
| PSoApp (n,args) ->
- GApp (CAst.make @@ GPatVar (true,n),
+ GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n),
List.map (glob_of_pat env sigma) args)
| PProd (na,t,c) ->
GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index eac8bd1a3..336cfac85 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1506,7 +1506,7 @@ let extract_explicit_arg imps args =
(**********************************************************************)
(* Main loop *)
-let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
+let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let rec intern env = CAst.with_loc_val (fun ?loc -> function
| CRef (ref,us) ->
let (c,imp,subscopes,l),_ =
@@ -1749,12 +1749,12 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
CAst.make ?loc @@
GHole (k, naming, solve)
(* Parsing pattern variables *)
- | CPatVar n when allow_patvar ->
+ | CPatVar n when pattern_mode ->
CAst.make ?loc @@
- GPatVar (true,n)
- | CEvar (n, []) when allow_patvar ->
+ GPatVar (Evar_kinds.SecondOrderPatVar n)
+ | CEvar (n, []) when pattern_mode ->
CAst.make ?loc @@
- GPatVar (false,n)
+ GPatVar (Evar_kinds.FirstOrderPatVar n)
(* end *)
(* Parsing existential variables *)
| CEvar (n, l) ->
@@ -1944,13 +1944,13 @@ let empty_ltac_sign = {
}
let intern_gen kind env
- ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
+ ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
c =
let tmp_scope = scope_of_type_kind kind in
internalize env {ids = extract_ids env; unb = false;
tmp_scope = tmp_scope; scopes = [];
impls = impls}
- allow_patvar (ltacvars, Id.Map.empty) c
+ pattern_mode (ltacvars, Id.Map.empty) c
let intern_constr env c = intern_gen WithoutTypeConstraint env c
@@ -2023,7 +2023,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
- ~allow_patvar:true ~ltacvars env c in
+ ~pattern_mode:true ~ltacvars env c in
pattern_of_glob_constr c
let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 644f60d85..324f7a389 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -83,7 +83,7 @@ val intern_constr : env -> constr_expr -> glob_constr
val intern_type : env -> constr_expr -> glob_constr
val intern_gen : typing_constraint -> env ->
- ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+ ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
constr_expr -> glob_constr
val intern_pattern : env -> cases_pattern_expr ->
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 835e94c77..ac0d96e96 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -8,6 +8,7 @@
open Names
open Globnames
+open Misctypes
(** The kinds of existential variable *)
@@ -16,6 +17,8 @@ open Globnames
type obligation_definition_status = Define of bool | Expand
+type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
+
type t =
| ImplicitArg of global_reference * (int * Id.t option)
* bool (** Force inference *)
@@ -27,6 +30,6 @@ type t =
| TomatchTypeParameter of inductive * int
| GoalEvar
| ImpossibleCase
- | MatchingVar of bool * Id.t
+ | MatchingVar of matching_var_kind
| VarInstance of Id.t
| SubEvar of Constr.existential_key
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 33c71884a..5da20c9d1 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -39,7 +39,7 @@ type glob_constr_r =
(** An identifier that cannot be regarded as "GRef".
Bound variables are typically represented this way. *)
| GEvar of existential_name * (Id.t * glob_constr) list
- | GPatVar of bool * patvar (** Used for patterns only *)
+ | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
| GApp of glob_constr * glob_constr list
| GLambda of Name.t * binding_kind * glob_constr * glob_constr
| GProd of Name.t * binding_kind * glob_constr * glob_constr
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1db8be081..bd2ac8c67 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -22,26 +22,10 @@ open Pltac
DECLARE PLUGIN "recdef_plugin"
-let pr_binding prc = function
- | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
-let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence prc l
- | ExplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
-let pr_with_bindings prc prlc (c,bl) =
- prc c ++ hv 0 (pr_bindings prc prlc bl)
-
let pr_fun_ind_using prc prlc _ opt_c =
match opt_c with
| None -> mt ()
- | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b)
+ | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
(* Duplication of printing functions because "'a with_bindings" is
(internally) not uniform in 'a: indeed constr_with_bindings at the
@@ -49,17 +33,12 @@ let pr_fun_ind_using prc prlc _ opt_c =
"constr with_bindings"; hence, its printer cannot be polymorphic in
(prc,prlc)... *)
-let pr_with_bindings_typed prc prlc (c,bl) =
- prc c ++
- hv 0 (pr_bindings prc prlc bl)
-
let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b ->
let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
- spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
-
+ spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
ARGUMENT EXTEND fun_ind_using
TYPED AS constr_with_bindings option
@@ -80,7 +59,6 @@ TACTIC EXTEND newfuninv
]
END
-
let pr_intro_as_pat _prc _ _ pat =
match pat with
| Some pat ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index aa8f918ae..785633e25 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1288,17 +1288,20 @@ let do_build_inductive
let t = EConstr.Unsafe.to_constr t in
evd,
Environ.push_named (LocalAssum (id,t))
- (* try *)
- (* Typing.e_type_of env evd (mkConstU c) *)
- (* with Not_found -> *)
- (* raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) *)
env
)
funnames
(Array.of_list funconstants)
(evd,Global.env ())
in
- let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
+ (* we solve and replace the implicits *)
+ let rta =
+ Array.mapi (fun i rt ->
+ let _,t = Typing.type_of env evd (EConstr.of_constr (mkConstU ((Array.of_list funconstants).(i)))) in
+ resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt
+ ) rta
+ in
+ let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
let env_with_graphs =
let rel_arity i funargs = (* Rebuilding arities (with parameters) *)
let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index b99f5a923..6fd496f50 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -707,3 +707,48 @@ let expand_as =
(loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
in
expand_as Id.Map.empty
+
+
+
+
+(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
+ *)
+
+exception Found of Evd.evar_info
+let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expected_type=Pretyping.WithoutTypeConstraint) env sigma rt =
+ let open Evd in
+ let open Evar_kinds in
+ (* we first (pseudo) understand [rt] and get back the computed evar_map *)
+ (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed.
+If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *)
+ let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Pretyping.empty_lvar expected_type rt in
+ let ctx, f = Evarutil.nf_evars_and_universes ctx in
+
+ (* then we map [rt] to replace the implicit holes by their values *)
+ let rec change rt =
+ match rt.CAst.v with
+ | GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *)
+ (
+ try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
+ Evd.fold (* to simulate an iter *)
+ (fun _ evi _ ->
+ match evi.evar_source with
+ | (loc_evi,ImplicitArg(gr_evi,p_evi,b_evi)) ->
+ if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi
+ then raise (Found evi)
+ | _ -> ()
+ )
+ ctx
+ ();
+ (* the hole was not solved : we do nothing *)
+ rt
+ with Found evi -> (* we found the evar corresponding to this hole *)
+ match evi.evar_body with
+ | Evar_defined c ->
+ (* we just have to lift the solution in glob_term *)
+ Detyping.detype false [] env ctx (EConstr.of_constr (f c))
+ | Evar_empty -> rt (* the hole was not solved : we do nothing *)
+ )
+ | _ -> Glob_ops.map_glob_constr change rt
+ in
+ change rt
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 25d79582f..99a258de9 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -119,3 +119,10 @@ val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr
val expand_as : glob_constr -> glob_constr
+
+
+(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
+ *)
+val resolve_and_replace_implicits :
+ ?flags:Pretyping.inference_flags ->
+ ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> glob_constr -> glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 143ce8288..a23c51495 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -142,7 +142,7 @@ let rec abstract_glob_constr c = function
let interp_casted_constr_with_implicits env sigma impls c =
Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
- ~allow_patvar:false c
+ c
(*
Construct a fixpoint as a Glob_term
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index f373e486c..bcfa6b931 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -26,31 +26,6 @@ open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
-(* Some pretty printing function for debugging purpose *)
-
-let pr_binding prc =
- function
- | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
- | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
-
-let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence prc l
- | ExplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
-
-let pr_with_bindings prc prlc (c,bl) =
- prc c ++ hv 0 (pr_bindings prc prlc bl)
-
-
-
-let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds =
- pr_with_bindings prc prc (c,bl)
-
(* The local debugging mechanism *)
(* let msgnl = Pp.msgnl *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d66298344..902985827 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -161,28 +161,6 @@ type 'a extra_genarg_printer =
| AnonHyp n -> int n
| NamedHyp id -> pr_id id
- let pr_binding prc = function
- | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
- let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ keyword "with" ++ brk (1,1) ++
- hv 0 (prlist_with_sep spc prc l)
- | ExplicitBindings l ->
- brk (1,1) ++ keyword "with" ++ brk (1,1) ++
- hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l)
- | NoBindings -> mt ()
-
- let pr_bindings_no_with prc prlc = function
- | ImplicitBindings l ->
- brk (0,1) ++
- prlist_with_sep spc prc l
- | ExplicitBindings l ->
- brk (0,1) ++
- prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
let pr_clear_flag clear_flag pp x =
match clear_flag with
| Some false -> surround (pp x)
@@ -190,7 +168,7 @@ type 'a extra_genarg_printer =
| None -> pp x
let pr_with_bindings prc prlc (c,bl) =
- prc c ++ pr_bindings prc prlc bl
+ prc c ++ Miscprint.pr_bindings prc prlc bl
let pr_with_bindings_arg prc prlc (clear_flag,c) =
pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
@@ -367,30 +345,6 @@ type 'a extra_genarg_printer =
| EvalConstRef sp ->
Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
- let pr_esubst prc l =
- let pr_qhyp = function
- (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
- | (_,(NamedHyp id,c)) ->
- str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
- in
- prlist_with_sep spc pr_qhyp l
-
- let pr_bindings_gen for_ex prc prlc = function
- | ImplicitBindings l ->
- spc () ++
- hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
- prlist_with_sep spc prc l)
- | ExplicitBindings l ->
- spc () ++
- hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
- pr_esubst prlc l)
- | NoBindings -> mt ()
-
- let pr_bindings prc prlc = pr_bindings_gen false prc prlc
-
- let pr_with_bindings prc prlc (c,bl) =
- hov 1 (prc c ++ pr_bindings prc prlc bl)
-
let pr_as_disjunctive_ipat prc ipatl =
keyword "as" ++ spc () ++
pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
@@ -1280,9 +1234,9 @@ let () =
(pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
Genprint.register_print0 wit_bindings
- (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
- (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it)));
+ (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
+ (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it)));
Genprint.register_print0 wit_constr_with_bindings
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
(pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 19bdf2d49..4265c416b 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -106,10 +106,6 @@ val pr_hintbases : string list option -> std_ppcmds
val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
-val pr_bindings :
- ('constr -> std_ppcmds) ->
- ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
-
val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 0096abfa6..d201cf949 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -189,7 +189,7 @@ let intern_binding_name ist x =
and if a term w/o ltac vars, check the name is indeed quantified *)
x
-let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
+let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c =
let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
let ltacvars = {
@@ -198,7 +198,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
ltac_extra = extra;
} in
let c' =
- warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
+ warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c
in
(c',if !strict_check then None else Some c)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2c09a8b69..2014f2aff 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -589,7 +589,7 @@ let interp_uconstr ist env sigma = function
} in
{ closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce }
-let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
+let interp_gen kind ist pattern_mode flags env sigma (c,ce) =
let constrvars = extract_ltac_constr_context ist env sigma in
let vars = {
Pretyping.ltac_constrs = constrvars.typed;
@@ -617,7 +617,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
} in
let kind_for_intern =
match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
- intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
+ intern_gen kind_for_intern ~pattern_mode ~ltacvars env c
in
(* Jason Gross: To avoid unnecessary modifications to tacinterp, as
suggested by Arnaud Spiwack, we run push_trace immediately. We do
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6fb1b6089..e53d19b59 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,6 +12,7 @@ open Nameops
open Globnames
open Misctypes
open Glob_term
+open Evar_kinds
(* Untyped intermediate terms, after ASTs and before constr. *)
@@ -59,6 +60,11 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
| CastNative t1, CastNative t2 -> eq t1 t2
| (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false
+let matching_var_kind_eq k1 k2 = match k1, k2 with
+| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
+| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2
+| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false
+
let tomatch_tuple_eq f (c1, p1) (c2, p2) =
let eqp (_, (i1, na1)) (_, (i2, na2)) =
eq_ind i1 i2 && List.equal Name.equal na1 na2
@@ -97,8 +103,7 @@ let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with
| GVar id1, GVar id2 -> Id.equal id1 id2
| GEvar (id1, arg1), GEvar (id2, arg2) ->
Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2
- | GPatVar (b1, pat1), GPatVar (b2, pat2) ->
- (b1 : bool) == b2 && Id.equal pat1 pat2
+ | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2
| GApp (f1, arg1), GApp (f2, arg2) ->
f f1 f2 && List.equal f arg1 arg2
| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 845ac4fb7..db2e5da95 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -143,7 +143,7 @@ let pattern_of_constr env sigma t =
match kind_of_term f with
| Evar (evk,args) ->
(match snd (Evd.evar_source evk sigma) with
- Evar_kinds.MatchingVar (true,id) -> Some id
+ Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
| _ -> None)
| _ -> None
with
@@ -156,13 +156,14 @@ let pattern_of_constr env sigma t =
pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
| Evar (evk,ctxt as ev) ->
(match snd (Evd.evar_source evk sigma) with
- | Evar_kinds.MatchingVar (b,id) ->
- assert (not b); PMeta (Some id)
+ | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
+ PMeta (Some id)
| Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
(* These are the two evar kinds used for existing goals *)
(* see Proofview.mark_in_evm *)
if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+ | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
PMeta None)
| Case (ci,p,a,br) ->
@@ -329,12 +330,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
| GVar id ->
(try PRel (List.index Name.equal (Name id) vars)
with Not_found -> PVar id)
- | GPatVar (false,n) ->
+ | GPatVar (Evar_kinds.FirstOrderPatVar n) ->
metas := n::!metas; PMeta (Some n)
| GRef (gr,_) ->
PRef (canonical_gr gr)
(* Hack to avoid rewriting a complete interpretation of patterns *)
- | GApp ({ CAst.v = GPatVar (true,n) }, cl) ->
+ | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
| GApp (c,cl) ->
PApp (pat_of_raw metas vars c,
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1d12b6d51..08a6dd4db 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -625,13 +625,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
inh_conv_coerce_to_tycon ?loc env evdref j tycon
- | GPatVar (someta,n) ->
+ | GPatVar kind ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
| None -> new_type_evar env evdref loc in
- let k = Evar_kinds.MatchingVar (someta,n) in
+ let k = Evar_kinds.MatchingVar kind in
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (k, naming, None) ->
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 360843711..a4ecbdf5e 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -47,3 +47,28 @@ let pr_move_location pr_id = function
| MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
| MoveFirst -> str " at top"
| MoveLast -> str " at bottom"
+
+(** Printing of bindings *)
+let pr_binding prc = function
+ | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+ | ImplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence prc l
+ | ExplicitBindings l ->
+ brk (1,1) ++ str "with" ++ brk (1,1) ++
+ pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_bindings_no_with prc prlc = function
+ | ImplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc prc l
+ | ExplicitBindings l ->
+ brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+ | NoBindings -> mt ()
+
+let pr_with_bindings prc prlc (c,bl) =
+ hov 1 (prc c ++ pr_bindings prc prlc bl)
+
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index fe8c779ff..dbbe3dcfd 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -22,3 +22,16 @@ val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
val pr_move_location :
('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+
+val pr_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_bindings_no_with :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+
+val pr_with_bindings :
+ ('a -> Pp.std_ppcmds) ->
+ ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds
+
diff --git a/stm/stm.ml b/stm/stm.ml
index 1ab22f642..739bc01e6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -474,10 +474,12 @@ end = struct (* {{{ *)
vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
- (match x with
+ (let rec aux x = match x with
| VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
| VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
- | _ -> "branch")
+ | VernacTime (_, e)
+ | VernacTimeout (_, e) -> aux e
+ | _ -> "branch" in aux x)
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
let get_info id =
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index d95eaabb8..4db744224 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -260,7 +260,7 @@ let mkGProd id c1 c2 = CAst.make @@
let mkGArrow c1 c2 = CAst.make @@
GProd (Anonymous, Explicit, c1, c2)
let mkGVar id = CAst.make @@ GVar (Id.of_string id)
-let mkGPatVar id = CAst.make @@ GPatVar((false, Id.of_string id))
+let mkGPatVar id = CAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id))
let mkGRef r = CAst.make @@ GRef (Lazy.force r, None)
let mkGAppRef r args = mkGApp (mkGRef r) args
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 12:14:39 +0000