diff options
| -rw-r--r-- | interp/constrintern.ml | 3 | ||||
| -rw-r--r-- | interp/constrintern.mli | 16 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 7 |
3 files changed, 16 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 75fda5d239..7431058849 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -186,6 +186,9 @@ let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map) impls +let extend_internalization_data (r, impls, scopes) impl scope = + (r, impls@[impl], scopes@[scope]) + (**********************************************************************) (* Contracting "{ _ }" in notations *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 9f06f16258..efbe7ec910 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -43,13 +43,12 @@ type var_internalization_type = | Method | Variable -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 *) - - Impargs.implicit_status list * (* signature of impargs of the variable *) - Notation_term.scope_name option list (* subscopes of the args of the variable *) +(** This collects relevant information for interning local variables: + - their coqdoc kind (a recursive call in a inductive, fixpoint of class; or a bound variable) + e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive + - their implicit arguments + - their argument scopes *) +type var_internalization_data (** A map of free variables to their implicit arguments and scopes *) type internalization_env = var_internalization_data Id.Map.t @@ -63,6 +62,9 @@ val compute_internalization_env : env -> evar_map -> ?impls:internalization_env Id.t list -> types list -> Impargs.manual_implicits list -> internalization_env +val extend_internalization_data : + var_internalization_data -> Impargs.implicit_status -> scope_name option -> var_internalization_data + type ltac_sign = { ltac_vars : Id.Set.t; (** Variables of Ltac which may be bound to a term *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 80e7e6ab96..5b29ab2092 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -195,13 +195,14 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let lift_lets = lift_rel_context 1 letbinders in let sigma, intern_body = let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in - let (r, impls, scopes) = + let interning_data = Constrintern.compute_internalization_data env sigma Constrintern.Recursive full_arity impls in let newimpls = Id.Map.singleton recname - (r, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))], - scopes @ [None]) in + (Constrintern.extend_internalization_data interning_data + (Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))) + None) in interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma ~impls:newimpls body (lift 1 top_arity) in |