aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/indrec.ml
Commit message (Collapse)AuthorAge
...
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Array.create is deprecatedGravatar pboutill2012-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of LabelGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing some str with strbrkGravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
* global_reference migrated from Libnames to new Globnames, less deps in ↵Gravatar letouzey2012-05-29
| | | | | | grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
| | | | | | | | | | as to ensure the warning is flushed in real time. Made systematic the use of if_warn instead of if_verbose when the warning is intended to signal something anormal (if_warn is activated when compiling verbosely and when working interactively while if_verbose is activated only when working interactively and when loading verbosely). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
| | | | | | | | | | Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refresh universes in params when generating schemes (Closes: #2429)Gravatar glondu2010-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
| | | | | | | Functions from Termops were sometimes fully qualified, sometimes not in the same module. This commit makes their usage more uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
| | | | | | | | | | | | | | | | | | | | | In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm property of "u" in the analysis of "t". Commutative cuts aren't compatible with typing so we need to ensure that term of "x"'s type and term of "u"'s have the same subterm_spec. Consequently,declaration.MRec argument has changed to the inductive name instead of only the number of the inductive in the mutual_inductive family. In subterm_specif and check_rec_call, arguments are stored in a stack. At each lambda, one element is popped to add in renv a smarter subterm_spec for the variable. subterm_spec of constructor's argument was added this way, the job is now done more often. Some eta contracted match branches are now accepted but enforcing eta-expansion of branches might be anyway a recommended invariant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new kind of automatically generated scheme "congr" for equality typesGravatar herbelin2009-08-23
| | | | | | | | (fixing and completing commit 12273). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
| | | | | | | | | very useful in practice but as soon as let-in's were not forbidden in the internal data structure, better to do it. Moreover, this gets closer to the view were inductive definitions are uniformly built from "contexts". (checker not changed!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
| | | | | | | | | | | | | | | (uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
* pushed evar reduction in kernelGravatar barras2009-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
| | | | | | | | | | | | | | | | | | | | | | | inductive types was not taken into account). - Virtually extended tauto to - support arbitrary-length disjunctions and conjunctions, - support arbitrary complex forms of disjunctions and conjunctions when in the contravariant of an implicative hypothesis, - stick with the purely propositional fragment and not apply reflexivity. This is virtual in the sense that it is not activated since it breaks compatibility with the existing tauto. - Modified the notion of conjunction and unit type used in hipattern in a way that is closer to the intuitive meaning (forbid dependencies between parameters in conjunction; forbid indices in unit types). - Investigated how far "iff" could be turned into a direct inductive definition; modified tauto.ml4 so that it works with the current and the alternative definition. - Fixed a bug in the error message from lookup_eliminator. - Other minor changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
| | | | | | | | | | | | Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk revision 11300). - Improved various error messages related to inversion, evars and case analysis (including the removal of the obsolete dependent/non dependent distinction). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
| | | | | | | | | | majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merged revisions ↵Gravatar msozeau2007-12-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1273, deuxième version (avec des shémas d'elimination ↵Gravatar notin2006-12-12
| | | | | | plus simples) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1273 (problème avec les paramètres non récursivement ↵Gravatar notin2006-12-12
| | | | | | uniformes dans le cas de types mutuellement inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵Gravatar herbelin2005-12-17
| | | | | | (suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵Gravatar herbelin2005-12-17
| | | | | | et suite correction bug #1028 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* parametres inductifsGravatar mohring2005-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Types inductifs parametriquesGravatar mohring2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation of function names about global references (especially, ↵Gravatar herbelin2005-02-18
| | | | | | renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expansion du prédicat du 'match' vis à vis de la dépendance en le terme ↵Gravatar herbelin2004-08-24
| | | | | | filtré (utilisation de Anonymous pour signaler une dépendance formelle, en relation avec le nommage dans Inductiveops.type_case_branches); uniformisation/nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Eta-expansion du predicat dans build_indrec (suite)Gravatar herbelin2004-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5887 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 00:06:14 +0000