| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) changed the semantics of rewrite H,H' : the earlier semantics
(rewrite H,H' == rewrite H; rewrite H') was poorly suited for
situations where first rewrite H generates side-conditions.
New semantics is tclTHENFIRST instead of tclTHEN, that is
side-conditions are left untouched.
Note to myself: check if side-effect-come-first bug of
setoid rewrite is still alive, and do something if yes
2) new syntax for rewriting something many times. This syntax is
shamelessly taken from ssreflect:
rewrite ?H means "H as many times as possible"
(i.e. almost repeat rewrite H, except that
possible side-conditions are left apart as in 1)
rewrite !H means "at least once" (i.e. rewrite H; repeat rewrite H)
rewrite 3?H means "up to 3 times", maybe less
(i.e. something like: do 3 (try rewrite H)).
rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H).
For instance: rewrite 3?foo, <-2!bar in H1,H2|-*
3) By the way, for a try, I've enabled the syntax +/- as synonyms for
->/<- in the orientation of rewrite.
Comments welcome ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10612 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
(Axiom/Variable...). New tactic clapply to apply unapplied class methods
in tactic mode, simple solution to the fact that apply does not work
up-to classes yet. Add Functions.v for class definitions related to
functional morphisms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10568 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
class_tactics for further customizations. Add Equivalence.v for
typeclass definitions on equivalences and clrewrite.v test-suite for
clrewrite. Debugging the tactic I found missing morphisms that are now
in Morphisms.v and removed some that made proof search fail or take too
long, not sure it's complete however.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10565 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10564 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
class_setoid to class_tactics...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place
d'une option "modulo_conv" pour contrôler l'usage de cette delta.
- Pour éviter que rewrite ne réussise trop souvent, la delta est
désactivée pour les tactiques d'élimination (une étude fine reste à faire).
- On n'utilise aussi delta que sur les sous-termes du problème
d'unification initial. C'est une heuristique qui est intuitive mais qui
reste à être évaluée.
- Au bilan, le surcoût en temps de compilation des theories est d'un
peu moins d'1%.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
"abstract" tactical is now as a regular ltac parameter of the
"identifier" type).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
trying to declare an instance with an already existing name. Add
possibility of not giving all the fields in Instance declarations, using
Refine.refine to generate the subgoals. No control over opacity in this
case though...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
only, and get rid of the "relation" definition which makes unification
fail blatantly. Replace it with a notation :) In its current state,
the new tactic seems ready for larger tests.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
eauto instead of an arbitrary tactic. Export more from eauto to allow
easier debugging.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
definition on which it is failing (useful for Program definitions and
others too).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10533 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
apply : si on a trouvé une méta, alors, on l'utilise pour instancier
les trous lors de la tentative de conversion modulo delta. Cela permet
ainsi de résoudre de petits cas d'unification, tel que celui annoncé
échouant dans le "beginner question" du 6 fevrier 2008 de coq-club.
Solde au passage de modifs cosmétiques de setoid_replace.ml avant
abandon probable du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10523 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10521 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
l'argument soit un type même lorsque c'était un terme qu'on
convertissait).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Tabareau:
- first pass: generation of the Morphism constraints with metavariables
for unspecified relations by one fold over the term.
This builds a "respect" proof term for the whole term with holes.
- second pass: constraint solving of the evars, taking care of finding a
solution for all the evars at once.
- third step: normalize proof term by found evars, apply it, done!
Works with any relation, currently not as efficient as it could be due
to bad handling of evars. Also needs some fine tuning of the instances
declared in Morphisms.v that are used during proof search, e.g. using
priorities.
Reorganize Classes.* accordingly, separating the setoids in
Classes.SetoidClass from the general morphisms in Classes.Morphisms
and the generally applicable relation theory in Classes.Relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
return a solution for the whole set of goals at once only. Add "debug
eauto" and "dfs eauto" syntaxes to get better control on the algorithm
from the surface interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10514 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10504 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
for basic functional programming and relation
definitions respectively.
Classes.Relations also includes the definition of Morphism
and instances for the standard morphisms and relations (eq, iff, impl,
inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic
has been reimplemented on top of these definitions, hence it doesn't
require a setoid implementation anymore. It also generates obligations
for missing reflexivity proofs, like the current setoid_rewrite. It has
not been tested on large examples but it should handle directions and
occurences. Works with in if no obligations are generated at this time.
What's missing is being able to rewrite by a lemma instead of a simple
hypothesis with no premises.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10496 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
maintenant écrire des fonctions récursives qui n'ont pas l'apparence
d'être fonctionnelle. La sémantique reste toutefois différente. Par
exemple, dans
Ltac is :=
let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
i.
l'évaluation de i est paresseuse, alors que dans une version non récursive
Ltac is :=
let i := match goal with |- ?A -> ?B => intro | _ => idtac end in
i.
l'évaluation de i est forte (et échoue sur le "match" qui n'est pas
autorisé à retourner une tactique).
(note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
document it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
tactics in SetoidClass
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10486 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10483 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
wrapper around Ltac program_simpl ::= .
!!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10451 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
hole kind info for topconstrs.
Derive eta_expansion from functional extensionality axiom.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10411 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
| |
Variable, et plus de trucs useless qui traînaient par ma faute (y
compris dans le noyau, la honte).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
instantiation of evars in tacticals (cf r9985, r10294).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10356 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Au passage, un peu plus de standardisation des noms de fonctions de
globalisation
Principe de base :
locate_foo : qualid -> foo (échoue avec Not_found)
global : reference -> global_reference (échoue avec UserError)
global_of_foo : foo -> global_reference (échoue avec UserError)
f_with_alias : se comporte comme f mais prenant aussi en compte les
notations de la forme "Notation id:=ref"
Principale exception :
locate, au lieu de locate_global
locate_global_with_alias, qui prend en entrée un "qualid located"
Restent beaucoup de fonctions qui pourraient utiliser
global_with_alias au lieu de global, notamment dans contribs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
10222: n'évaluer les std_ppcmds que si vraiment ils sont utilisés (en
particulier, les [< ... >] sont paresseux comme on l'attend mais pas
les ++).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10259 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
implicite du rapport de bug #468); utilisation pour cela d'un
mécanisme différent de localisation des échecs Ltac (mécanisme
probablement à affiner).
- Factorisation au passage des appels au débuggeur Ltac.
- Trivialités en passant dans clenv.ml.
- Tentative de documentation de l'infâme Reductionops.instance et essai
de déplacement plus amont du test "s = []".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10222 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
filtrage d'ordre 2 échoue à trouver un prédicat de réécriture qui
n'est pas une K-abstraction, les deux rewrite essaie alors le filtrage
d'ordre 1. Ce n'est pas le plus élégant mais c'est la solution
uniforme permettant d'être conservatif.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
(patch by J. Forest)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10212 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
decidability of the usual equality
Major changes:
* andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v
* added 2 files:
* toplevel/ind_tables.ml* : tables where the boolean eqs and the
decidability proofs are stored
* toplevel/auto_ind_decl.ml* : code of the schemes that are automatically
generated from inductives types (currently boolean eq & decidability )
* improvement of injection: if the decidability have been correctly computed,
injection can now break the equalities over dependant pair
How to use:
Set Equality Scheme. to set the automatic generation of the equality when you
create a new inductive type
Scheme Equality for I. tries to create the equality for the already declared
type I
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Ajout de l'option with à (e)destruct et (e)induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10162 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10157 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Printing Universes est active.
Ajout de l'option "using" à la tactique non documentée "auto decomp".
Ajout de la base "extcore" pour étendre "auto decomp" avec des
principes élémentaires tels que le dépliage de "iff".
Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10147 85f007b7-540e-0410-9357-904b9bb8a0f7
|