diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 10 | ||||
| -rw-r--r-- | engine/eConstr.mli | 15 | ||||
| -rw-r--r-- | engine/evarutil.ml | 10 | ||||
| -rw-r--r-- | engine/evarutil.mli | 10 | ||||
| -rw-r--r-- | engine/evd.ml | 10 | ||||
| -rw-r--r-- | engine/evd.mli | 14 | ||||
| -rw-r--r-- | engine/ftactic.ml | 10 | ||||
| -rw-r--r-- | engine/ftactic.mli | 10 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 10 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 10 | ||||
| -rw-r--r-- | engine/namegen.ml | 47 | ||||
| -rw-r--r-- | engine/namegen.mli | 16 | ||||
| -rw-r--r-- | engine/nameops.ml | 10 | ||||
| -rw-r--r-- | engine/nameops.mli | 10 | ||||
| -rw-r--r-- | engine/proofview.ml | 154 | ||||
| -rw-r--r-- | engine/proofview.mli | 31 | ||||
| -rw-r--r-- | engine/proofview_monad.ml | 40 | ||||
| -rw-r--r-- | engine/proofview_monad.mli | 31 | ||||
| -rw-r--r-- | engine/termops.ml | 14 | ||||
| -rw-r--r-- | engine/termops.mli | 17 | ||||
| -rw-r--r-- | engine/uState.ml | 10 | ||||
| -rw-r--r-- | engine/uState.mli | 10 | ||||
| -rw-r--r-- | engine/universes.ml | 10 | ||||
| -rw-r--r-- | engine/universes.mli | 10 | ||||
| -rw-r--r-- | engine/univops.ml | 10 | ||||
| -rw-r--r-- | engine/univops.mli | 10 |
26 files changed, 361 insertions, 178 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 9ac16b5b48..b95068ebf4 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6fa338c73d..36b6093d0f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CSig @@ -67,7 +69,10 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term val to_constr : Evd.evar_map -> t -> Constr.t -(** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) +(** Returns the evar-normal form of the argument, and cast it as a theoretically + evar-free term. In practice this function does not check that the result + is actually evar-free, it is currently the duty of the caller to do so. + This might change in the future. *) val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type diff --git a/engine/evarutil.ml b/engine/evarutil.ml index f82ffccdc3..7674cf67aa 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 923bf49a9c..373875bd05 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/engine/evd.ml b/engine/evd.ml index 2142cee374..e7d542d122 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/engine/evd.mli b/engine/evd.mli index 84fa70ef2f..ed3316c16d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -318,8 +320,8 @@ exception UniversesDiffer val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. - @raises UniversesDiffer in case a first-order unification fails. - @raises UniverseInconsistency + @raise UniversesDiffer in case a first-order unification fails. + @raise UniverseInconsistency . *) (** {5 Extra data} diff --git a/engine/ftactic.ml b/engine/ftactic.ml index 8e4c5f2206..e23a03c0c7 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Proofview.Notations diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 65ee929c8c..6c389b2d67 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module defines potentially focussing tactics. They are used by Ltac to diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 3674bb9432..4afa817b27 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the low-level monadic operations used by the diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 50b4abd8bd..545334ce9a 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file implements the low-level monadic operations used by the diff --git a/engine/namegen.ml b/engine/namegen.ml index ff0b5a74e7..b1a40aa18a 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created from contents that was formerly in termops.ml and @@ -190,9 +192,45 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (**********************************************************************) (* Fresh names *) +(* Introduce a mode where auto-generated names are mangled + to test dependence of scripts on auto-generated names *) + +let mangle_names = ref false + +let _ = Goptions.( + declare_bool_option + { optdepr = false; + optname = "mangle auto-generated names"; + optkey = ["Mangle";"Names"]; + optread = (fun () -> !mangle_names); + optwrite = (:=) mangle_names; }) + +let mangle_names_prefix = ref (Id.of_string "_0") +let set_prefix x = mangle_names_prefix := forget_subscript x + +let set_mangle_names_mode x = begin + set_prefix x; + mangle_names := true + end + +let _ = Goptions.( + declare_string_option + { optdepr = false; + optname = "mangled names prefix"; + optkey = ["Mangle";"Names";"Prefix"]; + optread = (fun () -> Id.to_string !mangle_names_prefix); + optwrite = begin fun x -> + set_prefix + (try Id.of_string x + with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) + end }) + +let mangle_id id = if !mangle_names then !mangle_names_prefix else id + (* Looks for next "good" name by lifting subscript *) let next_ident_away_from id bad = + let id = mangle_id id in let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id @@ -291,6 +329,7 @@ let next_global_ident_away id avoid = looks for same name with lower available subscript *) let next_ident_away id avoid = + let id = mangle_id id in if Id.Set.mem id avoid then next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id diff --git a/engine/namegen.mli b/engine/namegen.mli index abeed9f62d..0adbe5a51d 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file features facilities to generate fresh names. *) @@ -118,3 +120,9 @@ val compute_displayed_name_in_gen : (* Naming strategy for arguments in Prop when eliminating inductive types *) val use_h_based_elimination_names : unit -> bool + +(**********************************************************************) + +val set_mangle_names_mode : Id.t -> unit +(** Turn on mangled names mode and with the given prefix. + @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/nameops.ml b/engine/nameops.ml index 5105d7becc..53969cafa8 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/engine/nameops.mli b/engine/nameops.mli index 0fec8a925d..96842dfb99 100644 --- a/engine/nameops.mli +++ b/engine/nameops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/engine/proofview.ml b/engine/proofview.ml index c41b0b0dc5..8a844bbf54 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -33,7 +35,7 @@ type entry = (EConstr.constr * EConstr.types) list (* In this version: returns the list of focused goals together with the [evar_map] context. *) let proofview p = - p.comb , p.solution + List.map drop_state p.comb , p.solution let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in @@ -74,7 +76,7 @@ let dependent_init = let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; shelf = [] } + entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] } in fun t -> let entry, v = aux t in @@ -110,7 +112,7 @@ let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry) (* First component is a reverse list of the goals which come before and second component is the list of the goals which go after (in the expected order). *) -type focus_context = Evar.t list * Evar.t list +type focus_context = goal_with_state list * goal_with_state list (** Returns a stylised view of a focus_context for use by, for @@ -120,11 +122,12 @@ type focus_context = Evar.t list * Evar.t list new nearly identical function everytime. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) -let focus_context f = f +let focus_context (left,right) = + (List.map drop_state left, List.map drop_state right) (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns - [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the + [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the original list. The focused list has lenght [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises @@ -149,21 +152,35 @@ let unfocus_sublist (left,right) s = proofview. It returns the focused proofview, and a context for the focus stack. *) let focus i j sp = - let (new_comb, context) = focus_sublist i j sp.comb in - ( { sp with comb = new_comb } , context ) + let (new_comb, (left, right)) = focus_sublist i j sp.comb in + ( { sp with comb = new_comb } , (left, right) ) + +let cleared_alias evd g = + let evk = drop_state g in + let state = get_state g in + Option.map (fun g -> goal_with_state g state) (Evarutil.advance evd evk) (** [undefined defs l] is the list of goals in [l] which are still unsolved (after advancing cleared goals). Note that order matters. *) -let undefined defs l = +let undefined_evars defs l = List.fold_right (fun evk l -> match Evarutil.advance defs evk with | Some evk -> List.add_set Evar.equal evk l | None -> l) l [] +let goal_with_state_equal x y = Evar.equal (drop_state x) (drop_state y) +let undefined defs l = + List.fold_right (fun evk l -> + match cleared_alias defs evk with + | Some evk -> List.add_set goal_with_state_equal evk l + | None -> l) l [] (** Unfocuses a proofview with respect to a context. *) -let unfocus c sp = - { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } +let unfocus (left, right) sp = + { sp with comb = undefined sp.solution (unfocus_sublist (left, right) sp.comb) } +let with_empty_state = Proofview_monad.with_empty_state +let drop_state = Proofview_monad.drop_state +let goal_with_state = Proofview_monad.goal_with_state (** {6 The tactic monad} *) @@ -406,7 +423,8 @@ let tclFOCUSID id t = try let ev = Evd.evar_key id initial.solution in try - let n = CList.index Evar.equal ev initial.comb in + let comb = CList.map drop_state initial.comb in + let n = CList.index Evar.equal ev comb in (* goal is already under focus *) let (focused,context) = focus n n initial in Pv.set focused >> @@ -415,7 +433,7 @@ let tclFOCUSID id t = return result with Not_found -> (* otherwise, save current focus and work purely on the shelve *) - Comb.set [ev] >> + Comb.set [with_empty_state ev] >> t >>= fun result -> Comb.set initial.comb >> return result @@ -445,7 +463,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -462,7 +480,7 @@ let map_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -488,7 +506,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -532,7 +550,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match Evarutil.advance solution goal with + begin match cleared_alias solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -554,8 +572,8 @@ let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs (** [extend_to_list startxs rx endxs l] builds a list - [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises - [SizeMismatch] if [startxs@endxs] is already longer than [l]. *) + [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises + [SizeMismatch] if [startxs @ endxs] is already longer than [l]. *) let extend_to_list startxs rx endxs l = (* spiwack: I use [l] essentially as a natural number *) let rec duplicate acc = function @@ -624,12 +642,12 @@ let shelve = Comb.get >>= fun initial -> Comb.set [] >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.modify (fun gls -> gls @ initial) + Shelf.modify (fun gls -> gls @ CList.map drop_state initial) let shelve_goals l = let open Proof in Comb.get >>= fun initial -> - let comb = CList.filter (fun g -> not (CList.mem g l)) initial in + let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in Comb.set comb >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >> Shelf.modify (fun gls -> gls @ l) @@ -656,9 +674,27 @@ let free_evars sigma l = in List.map map l +let free_evars_with_state sigma l = + let cache = Evarutil.create_undefined_evars_cache () in + let map ev = + (** Computes the set of evars appearing in the hypotheses, the conclusion or + the body of the evar_info [evi]. Note: since we want to use it on goals, + the body is actually supposed to be empty. *) + let ev = drop_state ev in + let evi = Evd.find sigma ev in + let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in + (ev, fevs) + in + List.map map l + + (** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the result. *) +let unifiable_delayed_with_state sigma g l = + let g = drop_state g in + unifiable_delayed g l + let unifiable sigma g l = let l = free_evars sigma l in unifiable_delayed g l @@ -668,8 +704,8 @@ let unifiable sigma g l = whose definition other goals of [l] depend, and [n] are the non-unifiable goals. *) let partition_unifiable sigma l = - let fevs = free_evars sigma l in - CList.partition (fun g -> unifiable_delayed g fevs) l + let fevs = free_evars_with_state sigma l in + CList.partition (fun g -> unifiable_delayed_with_state sigma g fevs) l (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not @@ -680,7 +716,7 @@ let shelve_unifiable = let (u,n) = partition_unifiable initial.solution initial.comb in Comb.set n >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.modify (fun gls -> gls @ u) + Shelf.modify (fun gls -> gls @ CList.map drop_state u) (** [guard_no_unifiable] returns the list of unifiable goals if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) @@ -691,13 +727,14 @@ let guard_no_unifiable = match u with | [] -> tclUNIT None | gls -> - let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in + let l = CList.map (fun g -> Evd.dependent_evar_ident (drop_state g) initial.solution) gls in let l = CList.map (fun id -> Names.Name id) l in tclUNIT (Some l) (** [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) let unshelve l p = + let l = List.map with_empty_state l in (* advance the goals in case of clear *) let l = undefined p.solution l in { p with comb = p.comb@l } @@ -736,7 +773,7 @@ let with_shelf tac = let pgoal = Evd.principal_future_goal solution in let sigma = Evd.restore_future_goals sigma fgoals pgoal in (* Ensure we mark and return only unsolved goals *) - let gls' = undefined sigma (CList.rev_append gls' gls) in + let gls' = undefined_evars sigma (CList.rev_append gls' gls) in let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -818,7 +855,7 @@ let give_up = Comb.set [] >> mark_as_unsafe >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> - Giveup.put initial + Giveup.put (CList.map drop_state initial) @@ -859,8 +896,8 @@ module Progress = struct (** Equality function on goals *) let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in + let evi1 = Evd.find evars1 (drop_state gl1) in + let evi2 = Evd.find evars2 (drop_state gl2) in eq_evar_info evars1 evars2 evi1 evi2 end @@ -1027,27 +1064,35 @@ module Goal = struct env : Environ.env; sigma : Evd.evar_map; concl : EConstr.constr ; + state : StateStore.t; self : Evar.t ; (* for compatibility with old-style definitions *) } let assume (gl : t) = (gl : t) + let print { sigma; self } = { Evd.it = self; sigma } + + let state { state=state } = state + let env {env} = env let sigma {sigma} = sigma let hyps {env} = EConstr.named_context env let concl {concl} = concl let extra {sigma; self} = goal_extra sigma self - let gmake_with info env sigma goal = + let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; concl = EConstr.of_constr (Evd.evar_concl info); + state = state ; self = goal } let nf_gmake env sigma goal = + let state = get_state goal in + let goal = drop_state goal in let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in let sigma = Evd.add sigma goal info in - gmake_with info env sigma goal , sigma + gmake_with info env sigma goal state , sigma let nf_enter f = InfoL.tag (Info.Dispatch) begin @@ -1063,15 +1108,17 @@ module Goal = struct end end - let normalize { self } = + let normalize { self; state } = Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma self in + let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) let gmake env sigma goal = + let state = get_state goal in + let goal = drop_state goal in let info = Evd.find sigma goal in - gmake_with info env sigma goal + gmake_with info env sigma goal state let enter f = let f gl = InfoL.tag (Info.DBranch) (f gl) in @@ -1104,7 +1151,7 @@ module Goal = struct Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match Evarutil.advance sigma goal with + match cleared_alias sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1157,25 +1204,29 @@ let tclCHECKINTERRUPT = module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - let tactic tac = + let tactic ?(nf_evars=true) tac = (* spiwack: we ignore the dependencies between goals here, expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) let open Proof in Pv.get >>= fun ps -> try - let tac gl evd = + let tac g_w_s evd = + let g, w = drop_state g_w_s, get_state g_w_s in let glsigma = - tac { Evd.it = gl ; sigma = evd; } in + tac { Evd.it = g ; sigma = evd; } in let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in + let g = CList.map (fun g -> goal_with_state g w) glsigma.Evd.it in ( g, sigma ) in (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution + let (initgoals_w_state, initevd) = + Evd.Monad.List.map (fun g_w_s s -> + let g, w = drop_state g_w_s, get_state g_w_s in + let g, s = if nf_evars then goal_nf_evar s g else g, s in + goal_with_state g w, s) ps.comb ps.solution in - let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in + let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in let sgs = CList.flatten goalss in let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> @@ -1190,8 +1241,9 @@ module V82 = struct let nf_evar_goals = Pv.modify begin fun ps -> let map g s = goal_nf_evar s g in - let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { ps with solution = evd; comb = goals; } + let comb = CList.map drop_state ps.comb in + let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in + { ps with solution = evd; } end let has_unresolved_evar pv = @@ -1201,14 +1253,14 @@ module V82 = struct let grab pv = let undef = Evd.undefined_map pv.solution in let goals = CList.rev_map fst (Evar.Map.bindings undef) in - { pv with comb = goals } + { pv with comb = List.map with_empty_state goals } (* Returns the open goals of the proofview together with the evar_map to interpret them. *) let goals { comb = comb ; solution = solution; } = - { Evd.it = comb ; sigma = solution } + { Evd.it = List.map drop_state comb ; sigma = solution } let top_goals initial { solution=solution; } = let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in @@ -1222,9 +1274,9 @@ module V82 = struct let of_tactic t gls = try - let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } + { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in iraise (e, info) diff --git a/engine/proofview.mli b/engine/proofview.mli index 721ce507d4..4862791874 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This files defines the basic mechanism of proofs: the [proofview] @@ -72,7 +74,15 @@ val return : proofview -> Evd.evar_map val partial_proof : entry -> proofview -> constr list val initial_goals : entry -> (constr * types) list +(** goal <-> goal_with_state *) +val with_empty_state : + Proofview_monad.goal -> Proofview_monad.goal_with_state +val drop_state : + Proofview_monad.goal_with_state -> Proofview_monad.goal +val goal_with_state : + Proofview_monad.goal -> Proofview_monad.StateStore.t -> + Proofview_monad.goal_with_state (** {6 Focusing commands} *) @@ -416,14 +426,14 @@ module Unsafe : sig (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) - val tclNEWGOALS : Evar.t list -> unit tactic + val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) - val tclSETGOALS : Evar.t list -> unit tactic + val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Evar.t list tactic + val tclGETGOALS : Proofview_monad.goal_with_state list tactic (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic @@ -480,6 +490,7 @@ module Goal : sig val env : t -> Environ.env val sigma : t -> Evd.evar_map val extra : t -> Evd.Store.t + val state : t -> Proofview_monad.StateStore.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that @@ -504,6 +515,7 @@ module Goal : sig (** Compatibility: avoid if possible *) val goal : t -> Evar.t + val print : t -> Goal.goal Evd.sigma end @@ -540,7 +552,10 @@ val tclLIFT : 'a NonLogical.t -> 'a tactic (*** Compatibility layer with <= 8.2 tactics ***) module V82 : sig type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - val tactic : tac -> unit tactic + + (* [nf_evars=true] applies the evar (assignment) map to the goals + * (conclusion and context) before calling the tactic *) + val tactic : ?nf_evars:bool -> tac -> unit tactic (* normalises the evars in the goals, and stores the result in solution. *) diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index d0f4712258..52bcabf958 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the datatypes used as internal states by the @@ -149,13 +151,25 @@ module Info = struct CList.map_append (collapse_tree n) f end +module StateStore = Store.Make(struct end) + +(* let (set_state, get_state) = StateDyn.Easy.make_dyn "goal_state" *) + +type goal = Evar.t +type goal_with_state = Evar.t * StateStore.t + +let drop_state = fst +let get_state = snd +let goal_with_state g s = (g, s) +let with_empty_state g = (g, StateStore.empty) +let map_goal_with_state f (g, s) = (f g, s) (** Type of proof views: current [evar_map] together with the list of focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Evar.t list; - shelf : Evar.t list; + comb : goal_with_state list; + shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -169,7 +183,7 @@ module P = struct type e = bool (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list + type w = bool * goal list let wunit = true , [] let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2 @@ -209,9 +223,9 @@ module Solution : State with type t := Evd.evar_map = struct let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution }) end -module Comb : State with type t = Evar.t list = struct +module Comb : State with type t = goal_with_state list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal_with_state list let get = Logical.map (fun {comb} -> comb) Pv.get let set c = Pv.modify (fun pv -> { pv with comb = c }) let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb }) @@ -227,17 +241,17 @@ module Status : Writer with type t := bool = struct let put s = Logical.put (s, []) end -module Shelf : State with type t = Evar.t list = struct +module Shelf : State with type t = goal list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal list let get = Logical.map (fun {shelf} -> shelf) Pv.get let set c = Pv.modify (fun pv -> { pv with shelf = c }) let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) end -module Giveup : Writer with type t = Evar.t list = struct +module Giveup : Writer with type t = goal list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal list let put gs = Logical.put (true, gs) end diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index e7123218b1..9d75242175 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the datatypes used as internal states by the @@ -67,12 +69,21 @@ module Info : sig end +module StateStore : Store.S +type goal = Evar.t +type goal_with_state +val drop_state : goal_with_state -> goal +val get_state : goal_with_state -> StateStore.t +val goal_with_state : goal -> StateStore.t -> goal_with_state +val with_empty_state : goal -> goal_with_state +val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state + (** Type of proof views: current [evar_map] together with the list of focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Evar.t list; - shelf : Evar.t list; + comb : goal_with_state list; + shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -81,7 +92,7 @@ module P : sig type s = proofview * Environ.env (** Status (safe/unsafe) * given up *) - type w = bool * Evar.t list + type w = bool * goal list val wunit : w val wprod : w -> w -> w @@ -118,7 +129,7 @@ module Pv : State with type t := proofview module Solution : State with type t := Evd.evar_map (** Lens to the list of focused goals. *) -module Comb : State with type t = Evar.t list +module Comb : State with type t = goal_with_state list (** Lens to the global environment. *) module Env : State with type t := Environ.env @@ -128,11 +139,11 @@ module Status : Writer with type t := bool (** Lens to the list of goals which have been shelved during the execution of the tactic. *) -module Shelf : State with type t = Evar.t list +module Shelf : State with type t = goal list (** Lens to the list of goals which were given up during the execution of the tactic. *) -module Giveup : Writer with type t = Evar.t list +module Giveup : Writer with type t = goal list (** Lens and utilies pertaining to the info trace *) module InfoL : sig diff --git a/engine/termops.ml b/engine/termops.ml index 40b3d0d8b6..c615155d1f 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -797,9 +799,9 @@ let fold_constr_with_binders sigma g f n acc c = each binder traversal; it is not recursive and the order with which subterms are processed is not specified *) -let iter_constr_with_full_binders g f l c = +let iter_constr_with_full_binders sigma g f l c = let open RelDecl in - match kind c with + match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () | Cast (c,_, t) -> f l c; f l t diff --git a/engine/termops.mli b/engine/termops.mli index a3559a693b..ef3cb91be6 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines various utilities for term manipulation that are not @@ -76,9 +78,10 @@ val fold_constr_with_full_binders : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val iter_constr_with_full_binders : - (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> Constr.constr -> unit) -> 'a -> - Constr.constr -> unit +val iter_constr_with_full_binders : Evd.evar_map -> + (rel_declaration -> 'a -> 'a) -> + ('a -> constr -> unit) -> 'a -> + constr -> unit (**********************************************************************) diff --git a/engine/uState.ml b/engine/uState.ml index 625495866e..00825208b3 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/engine/uState.mli b/engine/uState.mli index 5c85b2b848..68fe350c01 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines universe unification states which are part of evarmaps. diff --git a/engine/universes.ml b/engine/universes.ml index f3660a5592..c744674053 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Sorts diff --git a/engine/universes.mli b/engine/universes.mli index 04586a6f85..8e6b8f60c9 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/engine/univops.ml b/engine/univops.ml index df25d87252..76dbaa250a 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ diff --git a/engine/univops.mli b/engine/univops.mli index 30fcc43681..d1585414c1 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr |