diff options
author | Matej Kosik <matej.kosik@inria.fr> | 2016-10-10 10:59:22 +0200 |
---|---|---|
committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-07 14:49:13 +0200 |
commit | 661940fd55a925a6f17f6025f5d15fc9f5647cf9 (patch) | |
tree | eee305047751a333fd8aeff625c775ce8ed58013 /intf/locus.mli | |
parent | 73fd3afba9e8917dfc0644d1d8d9b22063cfa2fe (diff) |
Put all plugins behind an "API".
Diffstat (limited to 'intf/locus.mli')
-rw-r--r-- | intf/locus.mli | 94 |
1 files changed, 0 insertions, 94 deletions
diff --git a/intf/locus.mli b/intf/locus.mli deleted file mode 100644 index 57b398ab4..000000000 --- a/intf/locus.mli +++ /dev/null @@ -1,94 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Misctypes - -(** Locus : positions in hypotheses and goals *) - -(** {6 Occurrences} *) - -type 'a occurrences_gen = - | AllOccurrences - | AllOccurrencesBut of 'a list (** non-empty *) - | NoOccurrences - | OnlyOccurrences of 'a list (** non-empty *) - -type occurrences_expr = (int or_var) occurrences_gen -type 'a with_occurrences = occurrences_expr * 'a - -type occurrences = int occurrences_gen - - -(** {6 Locations} - - Selecting the occurrences in body (if any), in type, or in both *) - -type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly - - -(** {6 Abstract clauses expressions} - - A [clause_expr] (and its instance [clause]) denotes occurrences and - hypotheses in a goal in an abstract way; in particular, it can refer - to the set of all hypotheses independently of the effective contents - of the current goal - - Concerning the field [onhyps]: - - [None] means *on every hypothesis* - - [Some l] means on hypothesis belonging to l *) - -type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag - -type 'id clause_expr = - { onhyps : 'id hyp_location_expr list option; - concl_occs : occurrences_expr } - -type clause = Id.t clause_expr - - -(** {6 Concrete view of occurrence clauses} *) - -(** [clause_atom] refers either to an hypothesis location (i.e. an - hypothesis with occurrences and a position, in body if any, in type - or in both) or to some occurrences of the conclusion *) - -type clause_atom = - | OnHyp of Id.t * occurrences_expr * hyp_location_flag - | OnConcl of occurrences_expr - -(** A [concrete_clause] is an effective collection of occurrences - in the hypotheses and the conclusion *) - -type concrete_clause = clause_atom list - - -(** {6 A weaker form of clause with no mention of occurrences} *) - -(** A [hyp_location] is an hypothesis together with a location *) - -type hyp_location = Id.t * hyp_location_flag - -(** A [goal_location] is either an hypothesis (together with a location) - or the conclusion (represented by None) *) - -type goal_location = hyp_location option - - -(** {6 Simple clauses, without occurrences nor location} *) - -(** A [simple_clause] is a set of hypotheses, possibly extended with - the conclusion (conclusion is represented by None) *) - -type simple_clause = Id.t option list - -(** {6 A notion of occurrences allowing to express "all occurrences - convertible to the first which matches"} *) - -type 'a or_like_first = AtOccs of 'a | LikeFirst - |