aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--checker/dune1
-rw-r--r--clib/hashset.ml6
-rw-r--r--doc/changelog/03-notations/11276-master+fix10750.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--interp/notation.ml4
-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/Notations2.v7
-rw-r--r--test-suite/success/implicit.v33
-rw-r--r--test-suite/success/specialize.v22
-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
23 files changed, 280 insertions, 127 deletions
diff --git a/Makefile b/Makefile
index d9fd03ac5a..c7d162bc56 100644
--- a/Makefile
+++ b/Makefile
@@ -284,7 +284,7 @@ cleanconfig:
distclean: clean cleanconfig cacheclean timingclean
voclean:
- find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \
+ find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \
-o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} +
find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} +
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/clib/hashset.ml b/clib/hashset.ml
index b7a245aed1..3477b615ef 100644
--- a/clib/hashset.ml
+++ b/clib/hashset.ml
@@ -118,8 +118,10 @@ module Make (E : EqType) =
t.table.(t.rover) <- emptybucket;
t.hashes.(t.rover) <- [| |];
end else begin
- Obj.truncate (Obj.repr bucket) (prev_len + 1) [@ocaml.alert "--deprecated"];
- Obj.truncate (Obj.repr hbucket) prev_len [@ocaml.alert "--deprecated"];
+ let newbucket = Weak.create prev_len in
+ Weak.blit bucket 0 newbucket 0 prev_len;
+ t.table.(t.rover) <- newbucket;
+ t.hashes.(t.rover) <- Array.sub hbucket 0 prev_len
end;
if len > t.limit && prev_len <= t.limit then t.oversize <- t.oversize - 1;
end;
diff --git a/doc/changelog/03-notations/11276-master+fix10750.rst b/doc/changelog/03-notations/11276-master+fix10750.rst
new file mode 100644
index 0000000000..a1b8594f5f
--- /dev/null
+++ b/doc/changelog/03-notations/11276-master+fix10750.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+ :cmd:`Print Visibility` was failing in the presence of only-printing notations
+ (`#11276 <https://github.com/coq/coq/pull/11276>`_,
+ by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_).
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/interp/notation.ml b/interp/notation.ml
index efb826a76e..5dc1658824 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1872,6 +1872,7 @@ let collect_notations stack =
| SingleNotation ntn ->
if List.mem_f notation_eq ntn knownntn then (all,knownntn)
else
+ try
let { not_interp = (_, r); not_location = (_, df) } =
NotationMap.find ntn (find_scope default_scope).notations in
let all' = match all with
@@ -1879,7 +1880,8 @@ let collect_notations stack =
(s,(df,r)::lonelyntn)::rest
| _ ->
(default_scope,[df,r])::all in
- (all',ntn::knownntn))
+ (all',ntn::knownntn)
+ with Not_found -> (* e.g. if only printing *) (all,knownntn))
([],[]) stack)
let pr_visible_in_scope prglob (scope,ntns) =
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/Notations2.v b/test-suite/success/Notations2.v
index d047f7560e..aa439fae12 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -165,3 +165,10 @@ Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pa
Check fun y : nat => # (x,z) ## y & y.
End M17.
+
+Module Bug10750.
+
+Notation "#" := 0 (only printing).
+Print Visibility.
+
+End Bug10750.
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/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-01 16:18:08 +0000