coq/contrib/recdef, branch master

menage dans funind + deplaceemnt de recdef dans funind

2008-04-28T12:17:22+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10865 85f007b7-540e-0410-9357-904b9bb8a0f7

Prise en compte des coercions dans les clauses "with" même si le type

2008-04-23T21:29:34+00:00

de l'argument donné contient des métavariables (souhait
#1408). Beaucoup d'infrastructure autour des constantes pour cela mais
qu'on devrait pouvoir récupérer pour analyser plus finement le
comportement des constantes en général :

1- Pour insérer les coercions, on utilise une transformation
   (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml.
2- Pour la compatibilité, on s'interdit d'insérer une coercion entre
   classes flexibles parce que sinon l'insertion de coercion peut prendre
   précédence sur la résolution des evars ce qui peut changer les 
   comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN).
3- Pour se souvenir rapidement de la nature flexible ou rigide du
   symbole de tête d'une constante vis à vis de l'évaluation, on met en
   place une table associant à chaque constante sa constante de tête (heads.ml)
4- Comme la table des constantes de tête a besoin de connaître
   l'opacité des variables de section, la partie tables de declare.ml va
   dans un nouveau decls.ml.

Au passage, simplification de coercion.ml, correction de petits bugs
(l'interface de Gset.fold n'était pas assez générale; specialize 
 cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml];
 whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml])
 et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml,
 classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7

Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.

2008-04-12T16:01:36+00:00

Uses setoid_rewrite even if rewriting with leibniz if there are
specified occurences, maybe a combination of pattern and rewrite could
be done instead. Correct spelling of occurrences.
Coq does not compile with this patch, the next one will make it compile
again.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10781 85f007b7-540e-0410-9357-904b9bb8a0f7

- Second pass on implementation of let pattern. Parse "let ' par [as x]?

2008-03-28T20:22:43+00:00

  [in I] := t [return pred] in b", just as SSReflect does with let:. 
  Change implementation: no longer a separate AST node, just add a case_style
  annotation on Cases to indicate it (if ML was dependently typed we
  could ensure that LetPatternStyle Cases have only one term to be
  matched and one branch, alas...). This factors out most code and we lose
  no functionality (win ! win !). Add LetPat.v test suite.

- Slight improvement of inference of return clauses for dependent
  pattern matching. If matching a variable of non-dependent type
  under a tycon that mentions it while giving no return clause, the
  dependency will be automatically infered. Examples at the end of
  DepPat. Should get rid of most explicit returns under tycons.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7

correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)

2008-03-08T16:05:33+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10640 85f007b7-540e-0410-9357-904b9bb8a0f7

Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from

2007-12-31T13:11:55+00:00

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

2007-12-06T17:36:14+00:00

devient Flags.




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7

minor bug correction in Function

2007-11-26T20:19:02+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10338 85f007b7-540e-0410-9357-904b9bb8a0f7

Correcting a segfault on amd64 arch with native compiler of ocaml 3.10

2007-11-13T17:04:27+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10319 85f007b7-540e-0410-9357-904b9bb8a0f7

Prise en compte des notations "alias" dans la globalisation des coercions.

2007-11-08T22:22:16+00:00

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