aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.ide6
-rw-r--r--checker/dune1
-rw-r--r--doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst4
-rw-r--r--ide/dune1
-rw-r--r--interp/constrintern.ml132
-rw-r--r--interp/impargs.ml27
-rw-r--r--interp/impargs.mli2
-rw-r--r--kernel/safe_typing.ml58
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/section.ml183
-rw-r--r--kernel/section.mli11
-rw-r--r--library/lib.ml21
-rw-r--r--plugins/ltac/rewrite.ml12
-rw-r--r--tactics/elimschemes.ml38
-rw-r--r--tactics/elimschemes.mli8
-rw-r--r--tactics/ind_tables.ml26
-rw-r--r--tactics/ind_tables.mli6
-rw-r--r--tactics/tactics.ml39
-rw-r--r--test-suite/bugs/opened/bug_3357.v7
-rw-r--r--test-suite/success/implicit.v33
-rw-r--r--test-suite/success/specialize.v22
-rw-r--r--toplevel/coqtop.ml18
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/indschemes.ml18
-rw-r--r--vernac/prettyp.ml6
26 files changed, 400 insertions, 287 deletions
diff --git a/Makefile.ide b/Makefile.ide
index bd72494289..b8a144f2ec 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -106,7 +106,7 @@ ifeq ($(HASCOQIDE),opt)
$(COQIDE): $(LINKIDEOPT)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
- -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 -linkall $(IDEFLAGS:.cma=.cmxa) $^
+ -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP_HIDE) $@
else
$(COQIDE): $(COQIDEBYTE)
@@ -116,7 +116,7 @@ endif
$(COQIDEBYTE): $(LINKIDE)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
- -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
+ -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
rm -f $@ && cp $< $@ && chmod a-w $@
@@ -241,7 +241,7 @@ $(COQIDEAPP)/Contents:
$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
- -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
+ -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP_HIDE) $@
$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
diff --git a/checker/dune b/checker/dune
index 73cbbc8d19..af7d4f2923 100644
--- a/checker/dune
+++ b/checker/dune
@@ -12,6 +12,7 @@
(executable
(name coqchk)
(public_name coqchk)
+ (modes exe byte)
(package coq)
(modules coqchk)
(flags :standard -open Coq_checklib)
diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst
new file mode 100644
index 0000000000..ecc134748d
--- /dev/null
+++ b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+ ``coqtop --version`` was broken when called in the middle of an installation process
+ (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing
+ `#11254 <https://github.com/coq/coq/pull/11254>`_).
diff --git a/ide/dune b/ide/dune
index a599be9351..12bad7ebc4 100644
--- a/ide/dune
+++ b/ide/dune
@@ -48,6 +48,7 @@
(package coqide)
(optional)
(modules coqide_main)
+ (modes exe byte)
(libraries coqide_gui))
; Input-method bindings
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ff115a3e48..c699f79351 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -256,7 +256,9 @@ type intern_env = {
unb: bool;
tmp_scope: Notation_term.tmp_scope_name option;
scopes: Notation_term.scope_name list;
- impls: internalization_env }
+ impls: internalization_env;
+ impl_binder_index: int option;
+}
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
@@ -317,27 +319,50 @@ let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
(**********************************************************************)
(* Utilities for binders *)
-let build_impls = function
- |Implicit -> (function
- |Name id -> Some (id, Impargs.Manual, (true,true))
- |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
- |Explicit -> fun _ -> None
-
-let impls_type_list ?(args = []) =
- let rec aux acc c = match DAst.get c with
- | GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
- | _ -> (Variable,[],List.append args (List.rev acc),[])
+
+let warn_shadowed_implicit_name =
+ CWarnings.create ~name:"shadowed-implicit-name" ~category:"syntax"
+ Pp.(fun na -> str "Making shadowed name of implicit argument accessible by position.")
+
+let exists_name na l =
+ match na with
+ | Name id -> List.exists (function Some (ExplByName id',_,_) -> Id.equal id id' | _ -> false) l
+ | _ -> false
+
+let build_impls ?loc n bk na acc =
+ match bk with
+ | Implicit ->
+ let na =
+ if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
+ else na in
+ let impl = match na with
+ | Name id -> Some (ExplByName id,Manual,(true,true))
+ | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
+ impl :: acc
+ | Explicit -> None :: acc
+
+let impls_binder_list =
+ let rec aux acc n = function
+ | (na,bk,None,_) :: binders -> aux (build_impls n bk na acc) (n+1) binders
+ | (na,bk,Some _,_) :: binders -> aux acc n binders
+ | [] -> (n,acc)
in aux []
-let impls_term_list ?(args = []) =
- let rec aux acc c = match DAst.get c with
- | GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+let impls_type_list n ?(args = []) =
+ let rec aux acc n c = match DAst.get c with
+ | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
+ | _ -> (Variable,[],List.rev acc,[])
+ in aux args n
+
+let impls_term_list n ?(args = []) =
+ let rec aux acc n c = match DAst.get c with
+ | GLambda (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c
| GRec (fix_kind, nas, args, tys, bds) ->
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
- let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
- aux acc' bds.(nb)
- |_ -> (Variable,[],List.append args (List.rev acc),[])
- in aux []
+ let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in
+ aux acc' n bds.(nb)
+ |_ -> (Variable,[],List.rev acc,[])
+ in aux args n
(* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
let rec check_capture ty = let open CAst in function
@@ -396,6 +421,14 @@ let remember_binders_impargs env bl =
let restore_binders_impargs env l =
List.fold_right pure_push_name_env l env
+let warn_unexpected_implicit_binder_declaration =
+ CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax"
+ Pp.(fun () -> str "Unexpected implicit binder declaration.")
+
+let check_implicit_meaningful ?loc k env =
+ if k = Implicit && env.impl_binder_index = None then
+ warn_unexpected_implicit_binder_declaration ?loc ()
+
let intern_generalized_binder intern_type ntnvars
env {loc;v=na} b' t ty =
let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
@@ -408,6 +441,7 @@ let intern_generalized_binder intern_type ntnvars
let env' = List.fold_left
(fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
env fvs in
+ check_implicit_meaningful ?loc b' env;
let bl = List.map
CAst.(map (fun id ->
(Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
@@ -423,8 +457,10 @@ let intern_generalized_binder intern_type ntnvars
| _ -> default_non_dependent_ident
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
- | _ -> na
- in (push_name_env ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
+ | _ -> na in
+ let impls = impls_type_list 1 ty' in
+ (push_name_env ntnvars impls env' (make ?loc na),
+ (make ?loc (na,b',ty')) :: List.rev bl)
let intern_assumption intern ntnvars env nal bk ty =
let intern_type env = intern (set_type_scope env) in
@@ -432,9 +468,10 @@ let intern_assumption intern ntnvars env nal bk ty =
| Default k ->
let ty = intern_type env ty in
check_capture ty nal;
- let impls = impls_type_list ty in
+ let impls = impls_type_list 1 ty in
List.fold_left
(fun (env, bl) ({loc;v=na} as locna) ->
+ check_implicit_meaningful ?loc k env;
(push_name_env ntnvars impls env locna,
(make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
@@ -457,7 +494,8 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd"
let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
let term = intern env def in
let ty = Option.map (intern env) ty in
- (push_name_env ntnvars (impls_term_list term) env locna,
+ let impls = impls_term_list 1 term in
+ (push_name_env ntnvars impls env locna,
(na,Explicit,term,ty))
let intern_cases_pattern_as_binder ?loc ntnvars env p =
@@ -1105,7 +1143,8 @@ let interp_reference vars r =
let (r,_,_,_),_ =
intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
{ids = Id.Set.empty; unb = false ;
- tmp_scope = None; scopes = []; impls = empty_internalization_env}
+ tmp_scope = None; scopes = []; impls = empty_internalization_env;
+ impl_binder_index = None}
Environ.empty_named_context_val
(vars, Id.Map.empty) None [] r
in r
@@ -1872,10 +1911,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* We add the recursive functions to the environment *)
let env_rec = List.fold_left_i (fun i en name ->
let (_,bli,tyi,_) = idl_temp.(i) in
- let bli = List.filter (fun (_, _, t, _) -> t = None) bli in
- let fix_args = List.map (fun (na, bk, t, _) -> build_impls bk na) bli in
- push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
- en (CAst.make @@ Name name)) 0 env lf in
+ let binder_index,fix_args = impls_binder_list 1 bli in
+ let impls = impls_type_list ~args:fix_args binder_index tyi in
+ push_name_env ntnvars impls en (CAst.make @@ Name name)) 0 env lf in
let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) ->
(* We add the binders common to body and type to the environment *)
let env_body = restore_binders_impargs env_rec before_impls in
@@ -1904,9 +1942,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(bl,intern_type env' ty,bl_impls)) dl in
let env_rec = List.fold_left_i (fun i en name ->
let (bli,tyi,_) = idl_tmp.(i) in
- let bli = List.filter (fun (_, _, t, _) -> t = None) bli in
- let cofix_args = List.map (fun (na, bk, _, _) -> build_impls bk na) bli in
- push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
+ let binder_index,cofix_args = impls_binder_list 1 bli in
+ push_name_env ntnvars (impls_type_list ~args:cofix_args binder_index tyi)
en (CAst.make @@ Name name)) 0 env lf in
let idl = Array.map2 (fun (_,_,_,bd) (b,c,bl_impls) ->
(* We add the binders common to body and type to the environment *)
@@ -1927,11 +1964,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in
expand_binders ?loc mkGLambda bl (intern env' c2)
| CLetIn (na,c1,t,c2) ->
- let inc1 = intern (reset_tmp_scope env) c1 in
- let int = Option.map (intern_type env) t in
+ let inc1 = intern_restart_implicit (reset_tmp_scope env) c1 in
+ let int = Option.map (intern_type_restart_implicit env) t in
DAst.make ?loc @@
GLetIn (na.CAst.v, inc1, int,
- intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
+ intern_restart_implicit (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
| CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
@@ -2114,7 +2151,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* Parsing existential variables *)
| CEvar (n, l) ->
DAst.make ?loc @@
- GEvar (n, List.map (on_snd (intern env)) l)
+ GEvar (n, List.map (on_snd (intern_no_implicit env)) l)
| CPatVar _ ->
raise (InternalizationError (loc,IllegalMetavariable))
(* end *)
@@ -2127,8 +2164,14 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
)
and intern_type env = intern (set_type_scope env)
+ and intern_no_implicit env = intern {env with impl_binder_index = None}
+
+ and intern_restart_implicit env = intern {env with impl_binder_index = Some 0}
+
+ and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0}
+
and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
- intern_local_binder_aux intern ntnvars env bind
+ intern_local_binder_aux intern_restart_implicit ntnvars env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
and intern_multiple_pattern env n pl =
@@ -2160,7 +2203,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
and intern_case_item env forbidden_names_for_gen (tm,na,t) =
(* the "match" part *)
- let tm' = intern env tm in
+ let tm' = intern_no_implicit env tm in
(* the "as" part *)
let extra_id,na =
let loc = tm'.CAst.loc in
@@ -2229,7 +2272,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let id = name_of_implicit imp in
let (_,a) = Id.Map.find id eargs in
let eargs' = Id.Map.remove id eargs in
- intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
+ intern_no_implicit enva a :: aux (n+1) impl' subscopes' eargs' rargs
with Not_found ->
if List.is_empty rargs && Id.Map.is_empty eargs && not (maximal_insertion_of imp) then
(* Less regular arguments than expected: complete *)
@@ -2241,7 +2284,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
) :: aux (n+1) impl' subscopes' eargs rargs
end
| (imp::impl', a::rargs') ->
- intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
+ intern_no_implicit enva a :: aux (n+1) impl' subscopes' eargs rargs'
| (imp::impl', []) ->
if not (Id.Map.is_empty eargs) then
(let (id,(loc,_)) = Id.Map.choose eargs in
@@ -2271,7 +2314,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| [] -> []
| a::args ->
let (enva,subscopes) = apply_scope_env env subscopes in
- (intern enva a) :: (intern_args env subscopes args)
+ (intern_no_implicit enva a) :: (intern_args env subscopes args)
in
try
@@ -2307,7 +2350,7 @@ let intern_gen kind env sigma
let tmp_scope = scope_of_type_kind sigma kind in
internalize env {ids = extract_ids env; unb = false;
tmp_scope = tmp_scope; scopes = [];
- impls = impls}
+ impls; impl_binder_index = Some 0}
pattern_mode (ltacvars, Id.Map.empty) c
let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
@@ -2389,7 +2432,8 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
{ Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
let tmp_scope = scope_of_type_kind sigma kind in
let impls = empty_internalization_env in
- internalize env {ids; unb = false; tmp_scope; scopes = []; impls}
+ internalize env
+ {ids; unb = false; tmp_scope; scopes = []; impls; impl_binder_index = Some 0}
pattern_mode (ltacvars, vl) c
let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
@@ -2397,7 +2441,8 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
- let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls}
+ let c = internalize env
+ {ids; unb = false; tmp_scope = None; scopes = []; impls; impl_binder_index = None}
false (empty_ltac_sign, vl) a in
(* Splits variables into those that are binding, bound, or both *)
(* Translate and check that [c] has all its free variables bound in [vars] *)
@@ -2433,7 +2478,8 @@ let intern_context env impl_env binders =
let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
(env, bl))
({ids = extract_ids env; unb = false;
- tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
+ tmp_scope = None; scopes = []; impls = impl_env;
+ impl_binder_index = Some 0}, []) binders in
(lenv.impls, List.map glob_local_binder_of_extended bl)
with InternalizationError (loc,e) ->
user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 2aa002ead1..df28b32f81 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,6 +20,7 @@ open Libobject
open EConstr
open Reductionops
open Namegen
+open Constrexpr
module NamedDecl = Context.Named.Declaration
@@ -289,7 +290,7 @@ type force_inference = bool (* true = always infer, never turn into evar/subgoal
type implicit_status =
(* None = Not implicit *)
- (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option
+ (explicitation * implicit_explanation * (maximal_insertion * force_inference)) option
type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
@@ -299,9 +300,12 @@ let is_status_implicit = function
| None -> false
| _ -> true
+let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
+
let name_of_implicit = function
| None -> anomaly (Pp.str "Not an implicit argument.")
- | Some (id,_,_) -> id
+ | Some (ExplByName id,_,_) -> id
+ | Some (ExplByPos (k,_),_,_) -> name_of_pos k
let maximal_insertion_of = function
| Some (_,_,(b,_)) -> b
@@ -336,7 +340,7 @@ let rec prepare_implicits f = function
| (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
| (Name id, Some imp)::imps ->
let imps' = prepare_implicits f imps in
- Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
+ Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits f imps
let set_manual_implicits flags enriching autoimps l =
@@ -346,15 +350,14 @@ let set_manual_implicits flags enriching autoimps l =
let imps' = merge (k+1) autoimps explimps in
begin match autoimp, explimp.CAst.v with
| (Name id,_), Some (_,max) ->
- Some (id, Manual, (set_maximality imps' max, true))
+ Some (ExplByName id, Manual, (set_maximality imps' max, true))
| (Name id,Some exp), None when enriching ->
- Some (id, exp, (set_maximality imps' flags.maximal, true))
+ Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
| (Name _,_), None -> None
| (Anonymous,_), Some (Name id,max) ->
- Some (id,Manual,(max,true))
+ Some (ExplByName id,Manual,(max,true))
| (Anonymous,_), Some (Anonymous,max) ->
- let id = Id.of_string ("arg_" ^ string_of_int k) in
- Some (id,Manual,(max,true))
+ Some (ExplByPos (k,None),Manual,(max,true))
| (Anonymous,_), None -> None
end :: imps'
| [], [] -> []
@@ -464,7 +467,7 @@ let implicits_of_global ref =
| [], _ -> []
| _, [] -> implicits
| Some (_, x,y) :: implicits, Name id :: names ->
- Some (id, x,y) :: rename implicits names
+ Some (ExplByName id, x,y) :: rename implicits names
| imp :: implicits, _ :: names -> imp :: rename implicits names
in
List.map (fun (t, il) -> t, rename il rename_l) l
@@ -494,7 +497,7 @@ let impls_of_context ctx =
let map decl =
let id = NamedDecl.get_id decl in
match Id.Map.get id !sec_implicits with
- | Glob_term.Implicit -> Some (id, Manual, (true, true))
+ | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
| Glob_term.Explicit -> None
in
List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
@@ -655,12 +658,12 @@ let compute_implicit_statuses autoimps l =
let rec aux i = function
| _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
| Name id :: autoimps, MaximallyImplicit :: manualimps ->
- Some (id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
+ Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
| Name id :: autoimps, Implicit :: manualimps ->
let imps' = aux (i+1) (autoimps, manualimps) in
let max = set_maximality imps' false in
if max then warn_set_maximal_deprecated i;
- Some (id, Manual, (max, true)) :: imps'
+ Some (ExplByName id, Manual, (max, true)) :: imps'
| Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
user_err ~hdr:"set_implicits"
(strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 8fa69e818a..ef3c2496f4 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -68,7 +68,7 @@ type maximal_insertion = bool (** true = maximal contextual insertion *)
type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
-type implicit_status = (Id.t * implicit_explanation *
+type implicit_status = (Constrexpr.explicitation * implicit_explanation *
(maximal_insertion * force_inference)) option
(** [None] = Not implicit *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 06f5aae047..759feda9ab 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -122,7 +122,7 @@ type section_data = {
type safe_environment =
{ env : Environ.env;
- sections : section_data Section.t;
+ sections : section_data Section.t option;
modpath : ModPath.t;
modvariant : modvariant;
modresolver : Mod_subst.delta_resolver;
@@ -159,7 +159,7 @@ let empty_environment =
revstruct = [];
modlabels = Label.Set.empty;
objlabels = Label.Set.empty;
- sections = Section.empty;
+ sections = None;
future_cst = [];
univ = Univ.ContextSet.empty;
engagement = None;
@@ -173,7 +173,7 @@ let is_initial senv =
| [], NONE -> ModPath.equal senv.modpath ModPath.initial
| _ -> false
-let sections_are_opened senv = not (Section.is_empty senv.sections)
+let sections_are_opened senv = not (Option.is_empty senv.sections)
let delta_of_senv senv = senv.modresolver,senv.paramresolver
@@ -323,6 +323,10 @@ let env_of_senv = env_of_safe_env
let sections_of_safe_env senv = senv.sections
+let get_section = function
+ | None -> CErrors.user_err Pp.(str "No open section.")
+ | Some s -> s
+
type constraints_addition =
| Now of Univ.ContextSet.t
| Later of Univ.ContextSet.t Future.computation
@@ -330,9 +334,7 @@ type constraints_addition =
let push_context_set poly cst senv =
if Univ.ContextSet.is_empty cst then senv
else
- let sections =
- if Section.is_empty senv.sections then senv.sections
- else Section.push_constraints cst senv.sections
+ let sections = Option.map (Section.push_constraints cst) senv.sections
in
{ senv with
env = Environ.push_context_set ~strict:(not poly) cst senv.env;
@@ -399,7 +401,7 @@ let check_current_library dir senv = match senv.modvariant with
(** When operating on modules, we're normally outside sections *)
let check_empty_context senv =
- assert (Environ.empty_context senv.env && Section.is_empty senv.sections)
+ assert (Environ.empty_context senv.env && Option.is_empty senv.sections)
(** When adding a parameter to the current module/modtype,
it must have been freshly started *)
@@ -447,22 +449,25 @@ let safe_push_named d env =
Environ.push_named d env
let push_named_def (id,de) senv =
- let sections = Section.push_local senv.sections in
+ let sections = get_section senv.sections in
+ let sections = Section.push_local sections in
let c, r, typ = Term_typing.translate_local_def senv.env id de in
let x = Context.make_annot id r in
let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
- { senv with sections; env = env'' }
+ { senv with sections=Some sections; env = env'' }
let push_named_assum (x,t) senv =
- let sections = Section.push_local senv.sections in
+ let sections = get_section senv.sections in
+ let sections = Section.push_local sections in
let t, r = Term_typing.translate_local_assum senv.env t in
let x = Context.make_annot x r in
let env'' = safe_push_named (LocalAssum (x,t)) senv.env in
- { senv with sections; env = env'' }
+ { senv with sections=Some sections; env = env'' }
let push_section_context (nas, ctx) senv =
- let sections = Section.push_context (nas, ctx) senv.sections in
- let senv = { senv with sections } in
+ let sections = get_section senv.sections in
+ let sections = Section.push_context (nas, ctx) sections in
+ let senv = { senv with sections=Some sections } in
let ctx = Univ.ContextSet.of_context ctx in
(* We check that the universes are fresh. FIXME: This should be done
implicitly, but we have to work around the API. *)
@@ -551,15 +556,18 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
| SFBmodule mb, M -> Modops.add_module mb senv.env
| _ -> assert false
in
- let sections = match sfb, gn with
- | SFBconst cb, C con ->
- let poly = Declareops.constant_is_polymorphic cb in
- Section.push_constant ~poly con senv.sections
- | SFBmind mib, I mind ->
- let poly = Declareops.inductive_is_polymorphic mib in
- Section.push_inductive ~poly mind senv.sections
- | _, (M | MT) -> senv.sections
- | _ -> assert false
+ let sections = match senv.sections with
+ | None -> None
+ | Some sections ->
+ match sfb, gn with
+ | SFBconst cb, C con ->
+ let poly = Declareops.constant_is_polymorphic cb in
+ Some (Section.push_constant ~poly con sections)
+ | SFBmind mib, I mind ->
+ let poly = Declareops.inductive_is_polymorphic mib in
+ Some (Section.push_inductive ~poly mind sections)
+ | _, (M | MT) -> Some sections
+ | _ -> assert false
in
{ senv with
env = env';
@@ -952,11 +960,11 @@ let open_section senv =
rev_objlabels = senv.objlabels;
} in
let sections = Section.open_section ~custom senv.sections in
- { senv with sections }
+ { senv with sections=Some sections }
let close_section senv =
let open Section in
- let sections0 = senv.sections in
+ let sections0 = get_section senv.sections in
let env0 = senv.env in
(* First phase: revert the declarations added in the section *)
let sections, entries, cstrs, revert = Section.close_section sections0 in
@@ -990,7 +998,7 @@ let close_section senv =
let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in
let senv = { senv with env; revstruct; sections; univ; objlabels; } in
(* Second phase: replay the discharged section contents *)
- let senv = add_constraints (Now cstrs) senv in
+ let senv = push_context_set false cstrs senv in
let modlist = Section.replacement_context env0 sections0 in
let cooking_info seg =
let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ae6993b0e2..0b7ca26e09 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -35,7 +35,7 @@ val is_initial : safe_environment -> bool
val env_of_safe_env : safe_environment -> Environ.env
-val sections_of_safe_env : safe_environment -> section_data Section.t
+val sections_of_safe_env : safe_environment -> section_data Section.t option
(** The safe_environment state monad *)
diff --git a/kernel/section.ml b/kernel/section.ml
index a1242f0faf..603ef5d006 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -20,7 +20,9 @@ type section_entry =
type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
-type 'a section = {
+type 'a t = {
+ sec_prev : 'a t option;
+ (** Section surrounding the current one *)
sec_context : int;
(** Length of the named context suffix that has been introduced locally *)
sec_mono_universes : ContextSet.t;
@@ -35,19 +37,9 @@ type 'a section = {
sec_custom : 'a;
}
-(** Sections can be nested with the proviso that no monomorphic section can be
- opened inside a polymorphic one. The reverse is allowed. *)
-type 'a t = 'a section list
+let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth prev
-let empty = []
-
-let is_empty = List.is_empty
-
-let depth = List.length
-
-let has_poly_univs = function
- | [] -> false
- | sec :: _ -> sec.has_poly_univs
+let has_poly_univs sec = sec.has_poly_univs
let find_emap e (cmap, imap) = match e with
| SecDefinition con -> Cmap.find con cmap
@@ -57,80 +49,59 @@ let add_emap e v (cmap, imap) = match e with
| SecDefinition con -> (Cmap.add con v cmap, imap)
| SecInductive ind -> (cmap, Mindmap.add ind v imap)
-let on_last_section f sections = match sections with
-| [] -> CErrors.user_err (Pp.str "No opened section")
-| sec :: rem -> f sec :: rem
-
-let with_last_section f sections = match sections with
-| [] -> f None
-| sec :: _ -> f (Some sec)
-
-let push_local s =
- let on_sec sec = { sec with sec_context = sec.sec_context + 1 } in
- on_last_section on_sec s
-
-let push_context (nas, ctx) s =
- let on_sec sec =
- if UContext.is_empty ctx then sec
- else
- let (snas, sctx) = sec.sec_poly_universes in
- let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
- { sec with sec_poly_universes; has_poly_univs = true }
- in
- on_last_section on_sec s
-
-let is_polymorphic_univ u s =
- let check sec =
- let (_, uctx) = sec.sec_poly_universes in
- Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx))
- in
- List.exists check s
-
-let push_constraints uctx s =
- let on_sec sec =
- if sec.has_poly_univs && Constraint.exists (fun (l,_,r) -> is_polymorphic_univ l s || is_polymorphic_univ r s) (snd uctx)
- then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
- let uctx' = sec.sec_mono_universes in
- let sec_mono_universes = (ContextSet.union uctx uctx') in
- { sec with sec_mono_universes }
- in
- on_last_section on_sec s
-
-let open_section ~custom sections =
- let sec = {
+let push_local sec =
+ { sec with sec_context = sec.sec_context + 1 }
+
+let push_context (nas, ctx) sec =
+ if UContext.is_empty ctx then sec
+ else
+ let (snas, sctx) = sec.sec_poly_universes in
+ let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
+ { sec with sec_poly_universes; has_poly_univs = true }
+
+let rec is_polymorphic_univ u sec =
+ let (_, uctx) = sec.sec_poly_universes in
+ let here = Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) in
+ here || Option.cata (is_polymorphic_univ u) false sec.sec_prev
+
+let push_constraints uctx sec =
+ if sec.has_poly_univs &&
+ Constraint.exists
+ (fun (l,_,r) -> is_polymorphic_univ l sec || is_polymorphic_univ r sec)
+ (snd uctx)
+ then CErrors.user_err
+ Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
+ let uctx' = sec.sec_mono_universes in
+ let sec_mono_universes = (ContextSet.union uctx uctx') in
+ { sec with sec_mono_universes }
+
+let open_section ~custom sec_prev =
+ {
+ sec_prev;
sec_context = 0;
sec_mono_universes = ContextSet.empty;
sec_poly_universes = ([||], UContext.empty);
- has_poly_univs = has_poly_univs sections;
+ has_poly_univs = Option.cata has_poly_univs false sec_prev;
sec_entries = [];
sec_data = (Cmap.empty, Mindmap.empty);
sec_custom = custom;
- } in
- sec :: sections
+ }
-let close_section sections =
- match sections with
- | sec :: sections ->
- sections, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom
- | [] ->
- CErrors.user_err (Pp.str "No opened section.")
+let close_section sec =
+ sec.sec_prev, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom
let make_decl_univs (nas,uctx) = abstract_universes nas uctx
-let push_global ~poly e s =
- if is_empty s then s
- else if has_poly_univs s && not poly
+let push_global ~poly e sec =
+ if has_poly_univs sec && not poly
then CErrors.user_err
Pp.(str "Cannot add a universe monomorphic declaration when \
section polymorphic universes are present.")
else
- let on_sec sec =
- { sec with
- sec_entries = e :: sec.sec_entries;
- sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data;
- }
- in
- on_last_section on_sec s
+ { sec with
+ sec_entries = e :: sec.sec_entries;
+ sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data;
+ }
let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
@@ -154,22 +125,16 @@ let extract_hyps sec vars used =
(* Only keep the part that is used by the declaration *)
List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
-let section_segment_of_entry vars e hyps sections =
+let section_segment_of_entry vars e hyps sec =
(* [vars] are the named hypotheses, [hyps] the subset that is declared by the
- global *)
- let with_sec s = match s with
- | None ->
- CErrors.user_err (Pp.str "No opened section.")
- | Some sec ->
- let hyps = extract_hyps sec vars hyps in
- let inst, auctx = find_emap e sec.sec_data in
- {
- abstr_ctx = hyps;
- abstr_subst = inst;
- abstr_uctx = auctx;
- }
- in
- with_last_section with_sec sections
+ global *)
+ let hyps = extract_hyps sec vars hyps in
+ let inst, auctx = find_emap e sec.sec_data in
+ {
+ abstr_ctx = hyps;
+ abstr_subst = inst;
+ abstr_uctx = auctx;
+ }
let segment_of_constant env con s =
let body = Environ.lookup_constant con env in
@@ -190,29 +155,19 @@ let extract_worklist info =
let args = instance_from_variable_context info.abstr_ctx in
info.abstr_subst, args
-let replacement_context env s =
- let with_sec sec = match sec with
- | None -> CErrors.user_err (Pp.str "No opened section.")
- | Some sec ->
- let cmap, imap = sec.sec_data in
- let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in
- let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in
- (cmap, imap)
- in
- with_last_section with_sec s
-
-let is_in_section env gr s =
- let with_sec sec = match sec with
- | None -> false
- | Some sec ->
- let open GlobRef in
- match gr with
- | VarRef id ->
- let vars = List.firstn sec.sec_context (Environ.named_context env) in
- List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
- | ConstRef con ->
- Cmap.mem con (fst sec.sec_data)
- | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
- Mindmap.mem ind (snd sec.sec_data)
- in
- with_last_section with_sec s
+let replacement_context env sec =
+ let cmap, imap = sec.sec_data in
+ let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con sec) cmap in
+ let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind sec) imap in
+ (cmap, imap)
+
+let is_in_section env gr sec =
+ let open GlobRef in
+ match gr with
+ | VarRef id ->
+ let vars = List.firstn sec.sec_context (Environ.named_context env) in
+ List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
+ | ConstRef con ->
+ Cmap.mem con (fst sec.sec_data)
+ | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
+ Mindmap.mem ind (snd sec.sec_data)
diff --git a/kernel/section.mli b/kernel/section.mli
index ec863b3b90..fbd3d8254e 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -16,13 +16,8 @@ open Univ
type 'a t
(** Type of sections with additional data ['a] *)
-val empty : 'a t
-
-val is_empty : 'a t -> bool
-(** Checks whether there is no opened section *)
-
val depth : 'a t -> int
-(** Number of nested sections (0 if no sections are open) *)
+(** Number of nested sections. *)
(** {6 Manipulating sections} *)
@@ -30,13 +25,13 @@ type section_entry =
| SecDefinition of Constant.t
| SecInductive of MutInd.t
-val open_section : custom:'a -> 'a t -> 'a t
+val open_section : custom:'a -> 'a t option -> 'a t
(** Open a new section with the provided universe polymorphic status. Sections
can be nested, with the proviso that polymorphic sections cannot appear
inside a monomorphic one. A custom data can be attached to this section,
that will be returned by {!close_section}. *)
-val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a
+val close_section : 'a t -> 'a t option * section_entry list * ContextSet.t * 'a
(** Close the current section and returns the entries defined inside, the set
of global monomorphic constraints added in this section, and the custom data
provided at the opening of the section. *)
diff --git a/library/lib.ml b/library/lib.ml
index c3c480aee4..6c47d6c6ae 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -133,7 +133,10 @@ let cwd () = !lib_state.path_prefix.Nametab.obj_dir
let current_mp () = !lib_state.path_prefix.Nametab.obj_mp
let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env())
-let sections_depth () = Section.depth (current_sections())
+let sections_depth () = match current_sections() with
+ | None -> 0
+ | Some sec -> Section.depth sec
+
let sections_are_opened = Global.sections_are_opened
let cwd_except_section () =
@@ -417,14 +420,18 @@ let extract_worklist info =
let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
+let force_sections () = match Safe_typing.sections_of_safe_env (Global.safe_env()) with
+ | Some s -> s
+ | None -> CErrors.user_err Pp.(str "No open section.")
+
let replacement_context () =
- Section.replacement_context (Global.env ()) (sections ())
+ Section.replacement_context (Global.env ()) (force_sections ())
let section_segment_of_constant con =
- Section.segment_of_constant (Global.env ()) con (sections ())
+ Section.segment_of_constant (Global.env ()) con (force_sections ())
let section_segment_of_mutual_inductive kn =
- Section.segment_of_inductive (Global.env ()) kn (sections ())
+ Section.segment_of_inductive (Global.env ()) kn (force_sections ())
let empty_segment = Section.empty_segment
@@ -437,8 +444,10 @@ let section_segment_of_reference = let open GlobRef in function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).Section.abstr_ctx
-let is_in_section ref =
- Section.is_in_section (Global.env ()) ref (sections ())
+let is_in_section ref = match sections () with
+ | None -> false
+ | Some sec ->
+ Section.is_in_section (Global.env ()) ref sec
let section_instance = let open GlobRef in function
| VarRef id ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2998e1c767..ca5c8b30c2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -924,10 +924,10 @@ let reset_env env =
let env' = Global.env_of_context (Environ.named_context_val env) in
Environ.push_rel_context (Environ.rel_context env) env'
-let fold_match ?(force=false) env sigma c =
+let fold_match env sigma c =
let (ci, p, c, brs) = destCase sigma c in
let cty = Retyping.get_type_of env sigma c in
- let dep, pred, exists, (sk,eff) =
+ let dep, pred, exists, sk =
let env', ctx, body =
let ctx, pred = decompose_lam_assum sigma p in
let env' = push_rel_context ctx env in
@@ -954,8 +954,8 @@ let fold_match ?(force=false) env sigma c =
else case_scheme_kind_from_type)
in
let exists = Ind_tables.check_scheme sk ci.ci_ind in
- if exists || force then
- dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
+ if exists then
+ dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind
else raise Not_found
in
let app =
@@ -964,7 +964,7 @@ let fold_match ?(force=false) env sigma c =
let meths = List.map (fun br -> br) (Array.to_list brs) in
applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
in
- sk, (if exists then env else reset_env env), app, eff
+ sk, (if exists then env else reset_env env), app
let unfold_match env sigma sk app =
match EConstr.kind sigma app with
@@ -1222,7 +1222,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
else
match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
| None -> state, c'
- | Some (cst, _, t', eff (*FIXME*)) ->
+ | Some (cst, _, t') ->
let state, res = aux { state ; env ; unfresh ;
term1 = t' ; ty1 = ty ;
cstr = (prop,cstr) ; evars } in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 51f01888aa..d6fda00ad8 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -24,14 +24,14 @@ open Ind_tables
(* Induction/recursion schemes *)
-let optimize_non_type_induction_scheme kind dep sort _ ind =
+let optimize_non_type_induction_scheme kind dep sort ind =
let env = Global.env () in
let sigma = Evd.from_env env in
if check_scheme kind ind then
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
appropriate type *)
- let cte, eff = find_scheme kind ind in
+ let cte = lookup_scheme kind ind in
let sigma, cte = Evd.fresh_constant_instance env sigma cte in
let c = mkConstU cte in
let t = type_of_constant_in (Global.env()) cte in
@@ -47,11 +47,11 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
let sigma, sort = Evd.fresh_sort_in_family sigma sort in
let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
let sigma = Evd.minimize_universes sigma in
- (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff
+ (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
else
let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
- (c, Evd.evar_universe_context sigma), Evd.empty_side_effects
+ (c, Evd.evar_universe_context sigma)
let build_induction_scheme_in_type dep sort ind =
let env = Global.env () in
@@ -60,17 +60,23 @@ let build_induction_scheme_in_type dep sort ind =
let sigma, c = build_induction_scheme env sigma pind dep sort in
c, Evd.evar_universe_context sigma
+let declare_individual_scheme_object name ?aux f =
+ let f : individual_scheme_object_function =
+ fun _ ind -> f ind, Evd.empty_side_effects
+ in
+ declare_individual_scheme_object name ?aux f
+
let rect_scheme_kind_from_type =
declare_individual_scheme_object "_rect_nodep"
- (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
+ (fun x -> build_induction_scheme_in_type false InType x)
let rect_scheme_kind_from_prop =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
- (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
+ (fun x -> build_induction_scheme_in_type false InType x)
let rect_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
- (fun _ x -> build_induction_scheme_in_type true InType x, Evd.empty_side_effects)
+ (fun x -> build_induction_scheme_in_type true InType x)
let rec_scheme_kind_from_type =
declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
@@ -90,7 +96,7 @@ let ind_scheme_kind_from_type =
let sind_scheme_kind_from_type =
declare_individual_scheme_object "_sind_nodep"
- (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
+ (fun x -> build_induction_scheme_in_type false InSProp x)
let ind_dep_scheme_kind_from_type =
declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
@@ -98,7 +104,7 @@ let ind_dep_scheme_kind_from_type =
let sind_dep_scheme_kind_from_type =
declare_individual_scheme_object "_sind" ~aux:"_sind_from_type"
- (fun _ x -> build_induction_scheme_in_type true InSProp x, Evd.empty_side_effects)
+ (fun x -> build_induction_scheme_in_type true InSProp x)
let ind_scheme_kind_from_prop =
declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
@@ -106,7 +112,7 @@ let ind_scheme_kind_from_prop =
let sind_scheme_kind_from_prop =
declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
- (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
+ (fun x -> build_induction_scheme_in_type false InSProp x)
let nondep_elim_scheme from_kind to_kind =
match from_kind, to_kind with
@@ -130,24 +136,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
let case_scheme_kind_from_type =
declare_individual_scheme_object "_case_nodep"
- (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
+ (fun x -> build_case_analysis_scheme_in_type false InType x)
let case_scheme_kind_from_prop =
declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
- (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
+ (fun x -> build_case_analysis_scheme_in_type false InType x)
let case_dep_scheme_kind_from_type =
declare_individual_scheme_object "_case" ~aux:"_case_from_type"
- (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
+ (fun x -> build_case_analysis_scheme_in_type true InType x)
let case_dep_scheme_kind_from_type_in_prop =
declare_individual_scheme_object "_casep_dep"
- (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
+ (fun x -> build_case_analysis_scheme_in_type true InProp x)
let case_dep_scheme_kind_from_prop =
declare_individual_scheme_object "_case_dep"
- (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
+ (fun x -> build_case_analysis_scheme_in_type true InType x)
let case_dep_scheme_kind_from_prop_in_prop =
declare_individual_scheme_object "_casep"
- (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
+ (fun x -> build_case_analysis_scheme_in_type true InProp x)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 093a4c456b..8e167b171c 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -12,14 +12,6 @@ open Ind_tables
(** Induction/recursion schemes *)
-val optimize_non_type_induction_scheme :
- 'a Ind_tables.scheme_kind ->
- Indrec.dep_flag ->
- Sorts.family ->
- 'b ->
- Names.inductive ->
- (Constr.constr * UState.t) * Evd.side_effects
-
val rect_scheme_kind_from_prop : individual scheme_kind
val ind_scheme_kind_from_prop : individual scheme_kind
val sind_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 9c94f3c319..517ccfaf53 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -82,10 +82,9 @@ let is_visible_name id =
with Not_found -> false
let compute_name internal id =
- match internal with
- | UserAutomaticRequest | UserIndividualRequest -> id
- | InternalTacticRequest ->
- Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
+ if internal then
+ Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
+ else id
let define internal role id c poly univs =
let id = compute_name internal id in
@@ -94,10 +93,7 @@ let define internal role id c poly univs =
let univs = UState.univ_entry ~poly ctx in
let entry = Declare.pure_definition_entry ~univs c in
let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
- let () = match internal with
- | InternalTacticRequest -> ()
- | _-> Declare.definition_message id
- in
+ let () = if internal then () else Declare.definition_message id in
kn, eff
let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
@@ -107,7 +103,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
let role = Evd.Schema (ind, kind) in
- let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
+ let internal = mode == InternalTacticRequest in
+ let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in
DeclareScheme.declare_scheme kind [|ind,const|];
const, Evd.concat_side_effects neff eff
@@ -125,7 +122,8 @@ let define_mutual_scheme_base kind suff f mode names mind =
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
let fold i effs id cl =
let role = Evd.Schema ((mind, i), kind)in
- let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
+ let internal = mode == InternalTacticRequest in
+ let cst, neff = define internal role id cl (Declareops.inductive_is_polymorphic mib) ctx in
(Evd.concat_side_effects neff effs, cst)
in
let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
@@ -153,6 +151,14 @@ let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
ca.(i), eff
+let define_individual_scheme kind mode names ind =
+ ignore (define_individual_scheme kind mode names ind)
+
+let define_mutual_scheme kind mode names mind =
+ ignore (define_mutual_scheme kind mode names mind)
+
let check_scheme kind ind =
try let _ = find_scheme_on_env_too kind ind in true
with Not_found -> false
+
+let lookup_scheme = DeclareScheme.lookup_scheme
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 7e544b09dc..d886fb67d3 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -45,15 +45,17 @@ val declare_individual_scheme_object : string -> ?aux:string ->
val define_individual_scheme : individual scheme_kind ->
internal_flag (** internal *) ->
- Id.t option -> inductive -> Constant.t * Evd.side_effects
+ Id.t option -> inductive -> unit
val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
- (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects
+ (int * Id.t) list -> MutInd.t -> unit
(** Main function to retrieve a scheme in the cache or to generate it *)
val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
val check_scheme : 'a scheme_kind -> inductive -> bool
+(** Like [find_scheme] but fails when the scheme is not already in the cache *)
+val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
val pr_scheme_kind : 'a scheme_kind -> Pp.t
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c44082cd88..9258a75461 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2982,14 +2982,17 @@ let quantify lconstr =
hypothesis of the goal, the new hypothesis replaces it.
(c,lbind) are supposed to be of the form
- ((t t1 t2 ... tm) , someBindings)
+ ((H t1 t2 ... tm) , someBindings)
+ whete t1..tn are user given args, to which someBinding must be combined.
- in which case we pose a proof with body
+ The goal is to pose a proof with body
- (fun y1...yp => H t1 t2 ... tm u1 ... uq) where yi are the
- remaining arguments of H that lbind could not resolve, ui are a mix
- of inferred args and yi. The overall effect is to remove from H as
- much quantification as possible given lbind. *)
+ (fun y1...yp => H t1 t2 ... tm u1 ... uq)
+
+ where yi are the remaining arguments of H that lbind could not
+ solve, ui are a mix of inferred args and yi. The overall effect
+ is to remove from H as much quantification as possible given
+ lbind. *)
let specialize (c,lbind) ipat =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -2998,6 +3001,7 @@ let specialize (c,lbind) ipat =
if lbind == NoBindings then
sigma, c
else
+ (* ***** SOLVING ARGS ******* *)
let typ_of_c = Retyping.get_type_of env sigma c in
(* If the term is lambda then we put a letin to put avoid
interaction between the term and the bindings. *)
@@ -3010,16 +3014,24 @@ let specialize (c,lbind) ipat =
let clause = clenv_unify_meta_types ~flags clause in
let sigma = clause.evd in
let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in
- let c_hd , c_args = decompose_app sigma c in
+ (* The completely applied term is (thd tstack), but tstack may
+ contain unsolved metas, so now we must reabstract them
+ args with there name to have
+ fun unsolv1 unsolv2 ... => (thd tstack_with _rels)
+ Note: letins have been reudced, they are not present in tstack *)
+ (* ****** REBUILDING UNSOLVED FORALLs ****** *)
+ (* thd is the thing to which we reapply everything, solved or
+ unsolved, unsolved things are requantified too *)
let liftrel x =
match kind sigma x with
| Rel n -> mkRel (n+1)
| _ -> x in
(* We grab names used in product to remember them at re-abstracting phase *)
- let typ_of_c_hd = pf_get_type_of gl c_hd in
+ let typ_of_c_hd = pf_get_type_of gl thd in
let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in
- (* accumulator args: arguments to apply to c_hd: all inferred
- args + re-abstracted rels *)
+ (* lprd = initial products (including letins).
+ l(tstack initially) = the same products after unification vs lbind (some metas remain)
+ args: accumulator : args to apply to hd: inferred args + metas reabstracted *)
let rec rebuild_lambdas sigma lprd args hd l =
match lprd , l with
| _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args))
@@ -3038,8 +3050,13 @@ let specialize (c,lbind) ipat =
| Context.Rel.Declaration.LocalAssum _::lp' , t::l' ->
let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in
sigma,hd'
+ | Context.Rel.Declaration.LocalDef _::lp' , _ ->
+ (* letins have been reduced in l and should anyway not
+ correspond to an arg, we ignore them. *)
+ let sigma,hd' = rebuild_lambdas sigma lp' args hd l in
+ sigma,hd'
| _ ,_ -> assert false in
- let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] c_hd tstack in
+ let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] thd tstack in
Evd.clear_metas sigma, hd
in
let typ = Retyping.get_type_of env sigma term in
diff --git a/test-suite/bugs/opened/bug_3357.v b/test-suite/bugs/opened/bug_3357.v
index c479158877..f0e5d71811 100644
--- a/test-suite/bugs/opened/bug_3357.v
+++ b/test-suite/bugs/opened/bug_3357.v
@@ -1,4 +1,9 @@
-Notation D1 := (forall {T : Type} ( x : T ) , Type).
+(* See discussion in #668 for whether manual implicit arguments should
+ be allowed in notations or not *)
+
+Set Warnings "+syntax".
+
+Fail Notation D1 := (forall {T : Type} ( x : T ) , Type).
Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33:
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 23853890d8..ecaaedca53 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -124,3 +124,36 @@ Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
(* Check global implicit declaration over ref not in section *)
Section D. Global Arguments eq [A] _ _. End D.
+
+(* Check local manual implicit arguments *)
+(* Gives a warning and make the second x anonymous *)
+(* Isn't the name "arg_1" a bit fragile though? *)
+
+Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+
+(* Check the existence of a shadowing warning *)
+
+Set Warnings "+syntax".
+Fail Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+Set Warnings "syntax".
+
+(* Test failure when implicit arguments are mentioned in subterms
+ which are not types of variables *)
+
+Set Warnings "+syntax".
+Fail Check (id (forall {a}, a)).
+Set Warnings "syntax".
+
+(* Miscellaneous tests *)
+
+Check let f := fun {x:nat} y => y=true in f false.
+
+(* Isn't the name "arg_1" a bit fragile, here? *)
+
+Check fun f : forall {_:nat}, nat => f (arg_1:=0).
+
+(* This test was wrongly warning/failing at some time *)
+
+Set Warnings "+syntax".
+Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
+Set Warnings "syntax".
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index f12db8b081..1b04594290 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -109,6 +109,28 @@ match goal with H:_ |- _ => clear H end.
match goal with H:_ |- _ => exact H end.
Qed.
+(* let ins should be supported in the type of the specialized hypothesis *)
+Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False.
+Goal False.
+ pose proof foo as P.
+ assert (2 = 2) as A by reflexivity.
+ specialize P with (1 := A).
+ assumption.
+Qed.
+
+(* Another more subtle test on letins: they should not interfere with foralls. *)
+Goal forall (P: forall y:nat,
+ forall A (zz:A),
+ let a := zz in
+ let x := 1 in
+ forall n : y = x,
+ n = n),
+ True.
+ intros P.
+ specialize P with (zz := @eq_refl _ 2).
+ constructor.
+Qed.
+
(* Test specialize as *)
Goal (forall x, x=0) -> 1=0.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 309f5b657a..46dd693155 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -155,12 +155,20 @@ let print_style_tags opts =
let () = List.iter iter tags in
flush_all ()
+let init_setup = function
+ | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+ | Some s -> Envars.set_user_coqlib s
+
let print_query opts = function
| PrintVersion -> Usage.version ()
| PrintMachineReadableVersion -> Usage.machine_readable_version ()
- | PrintWhere -> print_endline (Envars.coqlib ())
+ | PrintWhere ->
+ let () = init_setup opts.config.coqlib in
+ print_endline (Envars.coqlib ())
| PrintHelp h -> Usage.print_usage stderr h
- | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
+ | PrintConfig ->
+ let () = init_setup opts.config.coqlib in
+ Envars.print_config stdout Coq_config.all_src_dirs
| PrintTags -> print_style_tags opts.config
(** GC tweaking *)
@@ -188,10 +196,6 @@ let init_gc () =
Gc.minor_heap_size = 33554432; (* 4M *)
Gc.space_overhead = 120}
-let init_setup = function
- | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
- | Some s -> Envars.set_user_coqlib s
-
let init_process () =
(* Coq's init process, phase 1:
OCaml parameters, basic structures, and IO
@@ -256,11 +260,11 @@ type ('a,'b) custom_toplevel =
let init_toplevel custom =
let () = init_process () in
let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in
- let () = init_setup opts.config.coqlib in
(* Querying or running? *)
match opts.main with
| Queries q -> List.iter (print_query opts) q; exit 0
| Run ->
+ let () = init_setup opts.config.coqlib in
let customstate = init_execution opts (custom.init customopts) in
opts, customopts, customstate
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 310ea62a1d..f954915cf8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -430,7 +430,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
end
(* used in the bool -> leb side *)
-let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let open EConstr in
let avoid = Array.of_list aavoid in
let do_arg sigma hd v offset =
@@ -658,7 +658,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
then
Tacticals.New.tclTHEN
- (do_replace_bl mode bl_scheme_key ind
+ (do_replace_bl bl_scheme_key ind
(!avoid)
nparrec (ca.(2))
(ca.(1)))
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0e17f2b274..d48e2139d1 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -200,7 +200,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
Constrintern.Recursive full_arity impls
in
let newimpls = Id.Map.singleton recname
- (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+ (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
scopes @ [None]) in
interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
~impls:newimpls body (lift 1 top_arity)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b2e1a5e796..2f0b1062a7 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -210,7 +210,7 @@ let declare_one_case_analysis_scheme ind =
induction scheme, the other ones share the same code with the
appropriate type *)
if Sorts.family_leq InType kelim then
- ignore (define_individual_scheme dep UserAutomaticRequest None ind)
+ define_individual_scheme dep UserAutomaticRequest None ind
(* Induction/recursion schemes *)
@@ -248,7 +248,7 @@ let declare_one_induction_scheme ind =
else if depelim then kinds_from_type
else nondep_kinds_from_type)
in
- List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
+ List.iter (fun kind -> define_individual_scheme kind UserAutomaticRequest None ind)
elims
let declare_induction_schemes kn =
@@ -264,7 +264,7 @@ let declare_induction_schemes kn =
let declare_eq_decidability_gen internal names kn =
let mib = Global.lookup_mind kn in
if mib.mind_finite <> Declarations.CoFinite then
- ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
+ define_mutual_scheme eq_dec_scheme_kind internal names kn
let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind)
@@ -280,14 +280,14 @@ let try_declare_eq_decidability kn =
let declare_eq_decidability = declare_eq_decidability_scheme_with []
let ignore_error f x =
- try ignore (f x) with e when CErrors.noncritical e -> ()
+ try f x with e when CErrors.noncritical e -> ()
let declare_rewriting_schemes ind =
if Hipattern.is_inductive_equality ind then begin
- ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
- ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
- ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
- UserAutomaticRequest None ind);
+ define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind;
+ define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind;
+ define_individual_scheme rew_r2l_forward_dep_scheme_kind
+ UserAutomaticRequest None ind;
(* These ones expect the equality to be symmetric; the first one also *)
(* needs eq *)
ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
@@ -310,7 +310,7 @@ let declare_congr_scheme ind =
try Coqlib.check_required_library Coqlib.logic_module_name; true
with e when CErrors.noncritical e -> false
then
- ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
+ define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind
else
warn_cannot_build_congruence ()
end
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ea49cae9db..eb7b28f15b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -255,9 +255,13 @@ let needs_extra_scopes ref scopes =
let ty, _ctx = Typeops.type_of_global_in_context env ref in
aux env ty scopes
+let implicit_name_of_pos = function
+ | Constrexpr.ExplByName id -> Name id
+ | Constrexpr.ExplByPos (n,k) -> Anonymous
+
let implicit_kind_of_status = function
| None -> Anonymous, NotImplicit
- | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
+ | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
let dummy = {
Vernacexpr.implicit_status = NotImplicit;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:02:18 +0000