aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml12
-rw-r--r--interp/constrexpr_ops.ml5
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/constrintern.mli14
-rw-r--r--interp/declare.ml22
-rw-r--r--interp/dumpglob.mli1
-rw-r--r--interp/impargs.ml2
-rw-r--r--interp/impargs.mli1
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation.mli2
-rw-r--r--interp/notation_ops.ml6
-rw-r--r--interp/notation_term.ml4
13 files changed, 38 insertions, 37 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 77d612cfd9..757d186c8b 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -80,8 +80,8 @@ type cases_pattern_expr_r =
and cases_pattern_expr = cases_pattern_expr_r CAst.t
and cases_pattern_notation_substitution =
- cases_pattern_expr list * (** for constr subterms *)
- cases_pattern_expr list list (** for recursive notations *)
+ cases_pattern_expr list * (* for constr subterms *)
+ cases_pattern_expr list list (* for recursive notations *)
and constr_expr_r =
| CRef of qualid * instance_expr option
@@ -142,10 +142,10 @@ and local_binder_expr =
| CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
and constr_notation_substitution =
- constr_expr list * (** for constr subterms *)
- constr_expr list list * (** for recursive notations *)
- cases_pattern_expr list * (** for binders *)
- local_binder_expr list list (** for binder lists (recursive notations) *)
+ constr_expr list * (* for constr subterms *)
+ constr_expr list list * (* for recursive notations *)
+ cases_pattern_expr list * (* for binders *)
+ local_binder_expr list list (* for binder lists (recursive notations) *)
type constr_pattern_expr = constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3a4969a3ee..3a5af1dd5f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 =
in
List.equal field_eq l1 l2
| CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
- (** Don't care about the case_style *)
+ (* Don't care about the case_style *)
Option.equal constr_expr_eq r1 r2 &&
List.equal case_expr_eq a1 a2 &&
List.equal branch_expr_eq brl1 brl2
@@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with
| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
- (** Don't care about the [binder_kind] *)
+ (* Don't care about the [binder_kind] *)
List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
| _ -> false
@@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with
| h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll))
(** Folds and maps *)
-
let is_constructor id =
try Globnames.isConstructRef
(Smartlocate.global_of_extended_global
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fba03b9de9..0d0b6158d9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -960,7 +960,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
| GSort s -> CSort (extern_glob_sort s)
- | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *)
+ | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *)
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6313f2d7ba..40922b5c35 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1507,7 +1507,7 @@ let drop_notations_pattern looked_for genv =
let test_kind top =
if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
in
- (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+ (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
let rec rcp_of_glob scopes x = DAst.(map (function
| GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
| GHole (_,_,_) -> RCPatAtom (None)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 035e4bc644..61acd09d65 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -45,13 +45,15 @@ type var_internalization_type =
type var_internalization_data =
var_internalization_type *
- (** type of the "free" variable, for coqdoc, e.g. while typing the
- constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+ (* type of the "free" variable, for coqdoc, e.g. while typing the
+ constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+
Id.t list *
- (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
- in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
- Impargs.implicit_status list * (** signature of impargs of the variable *)
- Notation_term.scope_name option list (** subscopes of the args of the variable *)
+ (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+ in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+
+ Impargs.implicit_status list * (* signature of impargs of the variable *)
+ Notation_term.scope_name option list (* subscopes of the args of the variable *)
(** A map of free variables to their implicit arguments and scopes *)
type internalization_env = var_internalization_data Id.Map.t
diff --git a/interp/declare.ml b/interp/declare.ml
index a809a856b9..a0ebc3775e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -56,7 +56,7 @@ let load_constant i ((sp,kn), obj) =
(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn), obj) =
- (** Never open a local definition *)
+ (* Never open a local definition *)
if obj.cst_locl then ()
else
let con = Global.constant_of_delta_kn kn in
@@ -166,9 +166,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
export_seff ||
not de.const_entry_opaque ||
is_poly de ->
- (** This globally defines the side-effects in the environment. We mark
- exported constants as being side-effect not to redeclare them at
- caching time. *)
+ (* This globally defines the side-effects in the environment. We mark
+ exported constants as being side-effect not to redeclare them at
+ caching time. *)
let de, export = Global.export_private_constants ~in_section de in
export, ConstantEntry (PureEntry, DefinitionEntry de)
| _ -> [], ConstantEntry (EffectEntry, cd)
@@ -191,7 +191,6 @@ let declare_definition ?(internal=UserIndividualRequest)
(Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
(** Declaration of section variables and local definitions *)
-
type section_variable_entry =
| SectionLocalDef of Safe_typing.private_constants definition_entry
| SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
@@ -214,16 +213,16 @@ let cache_variable ((sp,_),o) =
| SectionLocalDef (de) ->
let (de, eff) = Global.export_private_constants ~in_section:true de in
let () = List.iter register_side_effect eff in
- (** The body should already have been forced upstream because it is a
- section-local definition, but it's not enforced by typing *)
+ (* The body should already have been forced upstream because it is a
+ section-local definition, but it's not enforced by typing *)
let (body, uctx), () = Future.force de.const_entry_body in
let poly, univs = match de.const_entry_universes with
| Monomorphic_const_entry uctx -> false, uctx
| Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
in
let univs = Univ.ContextSet.union uctx univs in
- (** We must declare the universe constraints before type-checking the
- term. *)
+ (* We must declare the universe constraints before type-checking the
+ term. *)
let () = Global.push_context_set (not poly) univs in
let se = {
secdef_body = body;
@@ -262,7 +261,6 @@ let declare_variable id obj =
oname
(** Declaration of inductive blocks *)
-
let declare_inductive_argument_scopes kn mie =
List.iteri (fun i {mind_entry_consnames=lc} ->
Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i));
@@ -360,7 +358,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
let id = Label.to_id label in
let univs = match univs with
| Monomorphic_ind_entry _ ->
- (** Global constraints already defined through the inductive *)
+ (* Global constraints already defined through the inductive *)
Monomorphic_const_entry Univ.ContextSet.empty
| Polymorphic_ind_entry (nas, ctx) ->
Polymorphic_const_entry (nas, ctx)
@@ -511,7 +509,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
load_function = load_univ_names;
open_function = open_univ_names;
discharge_function = discharge_univ_names;
- subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
+ subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
let declare_univ_binders gr pl =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 931d05a975..554da7603f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -18,6 +18,7 @@ val dump : unit -> bool
val noglob : unit -> unit
val dump_into_file : string -> unit (** special handling of "stdout" *)
+
val dump_to_dotglob : unit -> unit
val feedback_glob : unit -> unit
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d024a9e808..8a89bcdf26 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -448,7 +448,7 @@ let compute_mib_implicits flags kn =
Array.to_list
(Array.mapi (* No need to lift, arities contain no de Bruijn *)
(fun i mip ->
- (** No need to care about constraints here *)
+ (* No need to care about constraints here *)
let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
mib.mind_packets) in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ea5aa90f68..4afc2af5e9 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -65,6 +65,7 @@ type implicit_explanation =
operational only if [conclusion_matters] is true. *)
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 *
diff --git a/interp/notation.ml b/interp/notation.ml
index 0af75b5bfa..e17cc65042 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -308,7 +308,7 @@ let declare_delimiters scope key =
| None -> scope_map := String.Map.add scope newsc !scope_map
| Some oldkey when String.equal oldkey key -> ()
| Some oldkey ->
- (** FIXME: implement multikey scopes? *)
+ (* FIXME: implement multikey scopes? *)
Flags.if_verbose Feedback.msg_info
(str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
scope_map := String.Map.add scope newsc !scope_map
diff --git a/interp/notation.mli b/interp/notation.mli
index 3480d1c8f2..ab0501a1e1 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool
(** Open scope *)
val open_close_scope :
- (** locality *) bool * (* open *) bool * scope_name -> unit
+ (* locality *) bool * (* open *) bool * scope_name -> unit
(** Extend a list of scopes *)
val empty_scope_stack : scopes
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7a525f84a5..55a87fcd4d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -37,7 +37,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
| _ -> false)
| NApp (t1, a1), NApp (t2, a2) ->
(eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *)
| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
(eq_notation_constr vars) u1 u2 && b1 == b2
@@ -51,7 +51,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
let eqpat (p1, t1) (p2, t2) =
List.equal cases_pattern_eq p1 p2 &&
(eq_notation_constr vars) t1 t2
@@ -75,7 +75,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Option.equal (eq_notation_constr vars) o1 o2 &&
(eq_notation_constr vars) u1 u2 &&
(eq_notation_constr vars) r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
let eq (na1, o1, t1) (na2, o2, t2) =
Name.equal na1 na2 &&
Option.equal (eq_notation_constr vars) o1 o2 &&
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 5fb0ca1b43..0ef1f267f6 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -20,13 +20,13 @@ open Glob_term
as well as non global expressions such as existential variables. *)
type notation_constr =
- (** Part common to [glob_constr] and [cases_pattern] *)
+ (* Part common to [glob_constr] and [cases_pattern] *)
| NRef of GlobRef.t
| NVar of Id.t
| NApp of notation_constr * notation_constr list
| NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
| NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
- (** Part only in [glob_constr] *)
+ (* Part only in [glob_constr] *)
| NLambda of Name.t * notation_constr * notation_constr
| NProd of Name.t * notation_constr * notation_constr
| NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:49:19 +0000