diff options
Diffstat (limited to 'interp')
34 files changed, 97 insertions, 148 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 3ebbbdfb88..e4af0fcee0 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index bcb2f34377..8fce24249c 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index f1a8ed202f..3ed240d356 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 701c07dc8d..8573dccdf9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f09b316cd6..7b8b93377b 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e55f66e856..be8f99028c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -372,6 +372,9 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "a parameter of the inductive type; bound variables in " ++ strbrk "the type of a constructor shall use a different name.") +let pure_push_name_env (id,implargs) env = + {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + let push_name_env ?(global_level=false) ntnvars implargs env = let open CAst in function @@ -386,15 +389,23 @@ let push_name_env ?(global_level=false) ntnvars implargs env = set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var" else Dumpglob.dump_binding ?loc id; - {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + pure_push_name_env (id,implargs) env + +let remember_binders_impargs env bl = + List.map_filter (fun (na,_,_,_) -> + match na with + | Anonymous -> None + | Name id -> Some (id,Id.Map.find id env.impls)) bl + +let restore_binders_impargs env l = + List.fold_right pure_push_name_env l env let intern_generalized_binder ?(global_level=false) 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 let ty, ids' = - if t then ty, ids else - Implicit_quantifiers.implicit_application ids - Implicit_quantifiers.combine_params_freevar ty + if t then ty, ids + else Implicit_quantifiers.implicit_application ids ty in let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in @@ -1300,7 +1311,7 @@ let find_pattern_variable qid = if qualid_is_ident qid then qualid_basename qid else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) -let check_duplicate loc fields = +let check_duplicate ?loc fields = let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with @@ -1345,7 +1356,7 @@ let sort_fields ~complete loc fields completer = try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in - let () = check_duplicate loc fields in + let () = check_duplicate ?loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) @@ -1835,7 +1846,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in apply_impargs c env imp subscopes l loc - | CFix ({ CAst.loc = locid; v = iddef}, dl) -> + | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = @@ -1857,14 +1868,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = rbefore) recarg in let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in let bl = List.rev (List.map glob_local_binder_of_extended rbl) in - (n, bl, intern_type env' ty, env')) dl in - let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> (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 - (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in + let bl_impls = remember_binders_impargs env' bl in + (n, bl, intern_type env' ty, bl_impls)) dl in + (* 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 fix_args = (List.map (fun (na, bk, _, _) -> 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 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 + (n,bl,ty,intern {env_body with tmp_scope = None} bd)) dl idl_temp in DAst.make ?loc @@ GRec (GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), @@ -1884,15 +1899,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - (List.rev (List.map glob_local_binder_of_extended rbl), - intern_type env' ty,env')) dl in - let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (bli,tyi,_) = idl_tmp.(i) 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) - en (CAst.make @@ Name name)) 0 env' lf in - (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + let bl_impls = remember_binders_impargs env' bl in + (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 cofix_args = List.map (fun (na, bk, _, _) -> build_impls bk na) bli in + push_name_env ntnvars (impls_type_list ~args:cofix_args 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 *) + let env_body = restore_binders_impargs env_rec bl_impls in + (b,c,intern {env_body with tmp_scope = None} bd)) dl idl_tmp in DAst.make ?loc @@ GRec (GCoFix n, Array.of_list lf, diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4bf8ee9429..6c1f4898d9 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -189,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b (** Placeholder for global option, should be moved to a parameter *) val get_asymmetric_patterns : unit -> bool + +val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit +(** Check that a list of record field definitions doesn't contain + duplicates. *) diff --git a/interp/declare.ml b/interp/declare.ml index 17de06ed57..77313a54de 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/declare.mli b/interp/declare.mli index e2485d7cf0..0f64235048 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/deprecation.ml b/interp/deprecation.ml index b6f0dceb89..3b02ba4664 100644 --- a/interp/deprecation.ml +++ b/interp/deprecation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/deprecation.mli b/interp/deprecation.mli index aab87c11a2..f8083c2a5b 100644 --- a/interp/deprecation.mli +++ b/interp/deprecation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 274f9b851a..e1269025a4 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 554da7603f..18955985a0 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/genintern.ml b/interp/genintern.ml index 1b736b7977..e74f8d5f10 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/genintern.mli b/interp/genintern.mli index 4100f39029..5619a7b648 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/impargs.ml b/interp/impargs.ml index 112862da18..9977b29310 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/impargs.mli b/interp/impargs.mli index 92b6bdd406..90a7944642 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index bab9024415..9f6281ae15 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -23,9 +23,6 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) - module RelDecl = Context.Rel.Declaration (*i*) @@ -66,9 +63,6 @@ let declare_generalizable ~local gen = let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table -let ids_of_list l = - List.fold_right Id.Set.add l Id.Set.empty - let is_global id = try ignore (Nametab.locate_extended (qualid_of_ident id)); true with Not_found -> false @@ -105,26 +99,6 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c -let ids_of_names l = - List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l - -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = - let rec aux bdvars l c = match c with - ((CLocalAssum (n, _, c)) :: tl) -> - let bound = ids_of_names n in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - - | ((CLocalDef (n, c, t)) :: tl) -> - let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in - aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl - - | CLocalPattern _ :: tl -> assert false - | [] -> bdvars, l - in aux bound l binders - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs c = match DAst.get c with | GVar id -> @@ -149,7 +123,7 @@ let next_name_away_from na avoid = | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon") | Name id -> make_fresh avoid (Global.env ()) id -let combine_params avoid fn applied needed = +let combine_params avoid applied needed = let named, applied = List.partition (function @@ -167,47 +141,30 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false) named in - let is_unset (_, decl) = match decl with - | LocalAssum _ -> true - | LocalDef _ -> false - in - let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with - [], [] -> List.rev ids, avoid - | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named -> + | _, (_, LocalDef _) :: need -> aux ids avoid app need + + | [], [] -> List.rev ids, avoid + + | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need -> + | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need -> aux (x :: ids) avoid app need - | _, (Some cl, _ as d) :: need -> - let t', avoid' = fn avoid d in - aux (t' :: ids) avoid' app need - | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need - | [], (None, _ as decl) :: need -> - let t', avoid' = fn avoid decl in - aux (t' :: ids) avoid' app need + | _, (Some _, decl) :: need | [], (None, decl) :: need -> + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + let t' = CAst.make @@ CRef (qualid_of_ident id',None) in + aux (t' :: ids) (Id.Set.add id' avoid) app need | (x,_) :: _, [] -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") - in aux [] avoid applied needed - -let combine_params_freevar avoid (_, decl) = - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) - -let destClassApp cl = - let open CAst in - let loc = cl.loc in - match cl.v with - | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst) - | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst) - | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) - | _ -> raise Not_found + in + aux [] avoid applied needed let destClassAppExpl cl = let open CAst in @@ -217,7 +174,7 @@ let destClassAppExpl cl = | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found -let implicit_application env ?(allow_partial=true) f ty = +let implicit_application env ty = let is_class = try let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in @@ -230,24 +187,13 @@ let implicit_application env ?(allow_partial=true) f ty = match is_class with | None -> ty, env | Some ({CAst.loc;v=(id, par, inst)}, gr) -> - let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in + let avoid = Id.Set.union env (Id.Set.of_list (free_vars_of_constr_expr ty ~bound:env [])) in let env = Global.env () in let sigma = Evd.from_env env in let c = class_info env sigma gr in let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in + let args, avoid = combine_params avoid par pars in CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 437fef1753..4f9c47ec36 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,22 +11,14 @@ open Names open Glob_term open Constrexpr -open Libnames val declare_generalizable : local:bool -> lident list option -> unit -val ids_of_list : Id.t list -> Id.Set.t -val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t -val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t - (** Fragile, should be used only for construction a set of identifiers to avoid *) val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list -val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list - (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) @@ -37,15 +29,4 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits -val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t - -val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t) -> - constr_expr -> constr_expr * Id.Set.t - -(* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a +val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t diff --git a/interp/modintern.ml b/interp/modintern.ml index 2f516f4f3c..955288244e 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/modintern.mli b/interp/modintern.mli index 529c438c1a..75ab38c64a 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation.ml b/interp/notation.ml index cc06d5abfc..d58125e29b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation.mli b/interp/notation.mli index b32561d908..bd9b50977b 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 08619d912e..fdf12faa04 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 58fa221b16..7919d0061f 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 5024f5c26f..908455bd05 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/reserve.ml b/interp/reserve.ml index edbdf1dbba..e81439c3d5 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/reserve.mli b/interp/reserve.mli index a10858e71f..e180fc8071 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 91491bdf8d..74fe5d1c80 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index e41ef78913..d2770a2e73 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index bf3a8fe215..555eb34aed 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.mli b/interp/stdarg.mli index c974a4403c..dffbca0054 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 8df04187f1..302bb6ece2 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index e6e3b9cffa..0065b45b14 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |