| Age | Commit message (Collapse) | Author |
|---|
|
1. Genarg itself which only defines the abstract datatypes needed.
2. Genintern, first file of interp/, defining the intern and subst
functions.
3. Geninterp, first file of tactics/, defining the interp function.
4. Genprint, first file of printing/, dealing with the printers.
The Genarg file has no dependency and is in lib/, so that we can put
generic arguments everywhere, and in particular in ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
related types. This will ultimately allow putting genargs into
these ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
their own file, Stdarg.
This required a little trick to correctly handle wit_* naming. We
use a dynamic table to remember exactly where those arguments come
from.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
structure. The code is quite dumb for now, as it only handles basic
extended generig arguments (ExtraArgTypes). Soon, code from other
modules will be centralized there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
upto Genarg, so moved them there. This will allow defining the new
genarg interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16575 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
arguments. That way we will be able to define interpretation of
tactics without referring to tactic values.
Quite ad-hoc for now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16565 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Now, instead of having three unrelated types describing a dynamic
type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type"
whose parameters describe the reified type at each level.
This has various advantages:
- No more code duplication to handle the three level separately;
- Safer code: one is not authorized to mix unrelated types when what
was morally expected was a genarg_type.
- Each level-specialized representation can be accessed through
well-typed projections: rawwit, glbwit and topwit.
Documenting a bit Genarg b.t.w.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16564 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15380 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Stuff about reductions now in genredexpr.mli, operations in redops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactic arguments of ltac functions).
Added support for recursive entries in ARGUMENT EXTEND, for right-hand
sides of ARGUMENT EXTEND raising exceptions and for right-hand sides
referring to "loc". Also fixed parsing level of initial value in
create_arg (raw instead of glob). Thanks to the Ssreflect plugin for
revealing these problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15065 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an
Ltac function - see Tacinterp.add_primitive_tactic).
More precisely, when parsing "f ref" and "ref" is recognized as the
name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic
(like "eauto", "firstorder", "discriminate", ...), the code was
correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END'
was given (where "foo" has no arguments in the rule) but not when a rule
of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given
(where "foo" had an optional argument in the rule). In particular,
"firstorder" was in this case.
More generally, if, for an extra argument able to parse the empty string, a rule
`TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given,
then "foo" was not recognized as parseable as an atomic string (this
happened e.g. for "eauto"). This is now also fixed.
There was also another bug when the internal name of tactic was not
the same as the user-level name of the tactic. This is the reason why
"congruence" was not recognized when given as argument of an ltac (its
internal name is "cc").
Incidentally removed the redundant last line in the parsing rule for
"firstorder".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat
tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\
W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s
/glob_terms?/glob_constr/g' **/*.ml*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13745 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
There was a discrepancy of the notions "raw" and "globalized" between
constrs and tactics, and some confusion of the notions in
e.g. genarg.mli (see all globwit_* there). This commit is a first step
towards unification of terminology between constrs and
tactics. Changes in module names will be done separately.
In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even
affected by this change, has not been touched and highlights another
confusion in "ARGUMENT EXTEND" in general that will be addressed
later.
The funind plugin doesn't respect the same naming conventions as the
rest, so leave some "raw" there for now... they will be addressed
later.
This big commit has been generated with the following command (wrapped
here, but should be on a *single* line):
perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder|
_context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo
b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam
bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G
\2/g' `git ls-files|grep -v dev/doc/changes.txt`
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- 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
|
|
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
the general sigma of the goal so that tactics have no such low-level
tclEVARS, Evd.merge, or check_evars to do:
- what takes tclEVARS and check_evars in charge is now a new
tactical of name tclWITHHOLES (this tactical has a flag to support
tactics in either the "e"- mode and the non "e"- mode);
- the merge of goal evars and holes is now done generically at
interpretation time (in tacinterp) and as a side-effect it also
anticipates the possibility to refer to evars of the goal in the
arguments;
- with this approach, we don't need such constr/open_constr or
bindings/ebindings variants and we can get rid of all ugly
inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
this is the case e.g. of "rewrite !c" which morally reevaluates c at
each new rewriting step; this kind of tactics still receive a
specific sigma around their arguments and they have to merge evars
and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
types so that the type of terms in Genarg can be changed w/o in full
independence of the level.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12599 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
string in most commands expecting a global name (e.g. 'Print "+"' for
an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation,
possibly surrounded by a scope delimiter). Support for such smart
globals in VERNAC EXTEND to do.
Added a file smartlocate.ml for high-level globalization functions.
Mini-nettoyage metasyntax.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- "*" implements Arthur Charguéraud's "introv"
- "**" works as "; intros" (see also "*" in ssreflect).
- Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui.
- Shy attempt to seize the opportunity to clean Zarith_dec but Coq's
library is really going anarchically (see a summary of the various
formulations of total order, dichotomy of order and decidability of
equality and in stdlib-project.tex in branch V8revised-theories).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Extension du test de réversibilité acyclique des notations dures aux
notations de type abbréviation (du genre inhabited A := A).
- Ajout options Local/Global à Transparent/Opaque.
- Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé
dependent retiré).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
SearchAbout + referring objects by their notation).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction divers messages d'erreur
- lorsque rien à réécrire dans une hyp,
- lorsqu'une variable ltac n'est pas liée,
- correction anomalie en présence de ?id dans le "as" de induction,
- correction mauvais env dans message d'erreur de unify_0.
- Diverses extensions et améliorations
- "specialize" :
- extension au cas (fun x1 ... xn => H u1 ... un),
- renommage au même endroit.
- "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
- "induction"
- intro des IH toujours au sommet même si induction sur var quantifiée,
- ajout d'un hack pour la reconnaissance de schémas inductifs comme
N_ind_double mais il reste du boulot pour reconnaître (et/ou
réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
dans l'ordre standard,
- vérification de longueur et éventuelle complétion des
intropatterns dans le cas de sous-patterns destructifs dans induction
(par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
le n dans le contexte),
- localisation des erreurs d'intropattern,
- ajout d'un pattern optionnel après "as" pour forcer une égalité et la
nommer (*).
- "apply" accepte plusieurs arguments séparés par des virgules (*).
- Plus de robustesse pour clear en présence d'evars.
- Amélioration affichage TacFun dans Print Ltac.
- Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
(incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
- Fusion VTactic/VFun dans l'espoir.
- Mise en place d'un système de trace de la pile des appels Ltac (tout en
préservant certains aspects de la récursivité terminale - cf bug #468).
- Tactiques primitives
- ajout de "move before" dans les tactiques primitives et ajout des
syntaxes move before et move dependent au niveau utilisateur (*),
- internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
- suppression de Intro_replacing et du code sous-traitant
- Nettoyage
- Suppression cible et fichiers minicoq non portés depuis longtemps.
(*) Extensions de syntaxe qu'il pourrait être opportun de discuter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
effacé dans un intro-pattern (suggéré par ssreflect).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- ajout de -> et <- pour substitution immédiate d'une égalité
(comportement à la subst si variable, à la rewrite in * sinon)
- ajout possibilité d'hypothèses avec paramètres
- correction d'un comportement bizarre de l'utilisation des noms dans
cas "[[|] H]" (cf CHANGES)
Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])"
pour décider de garder les noms, mais la syntaxe est assez
moche. Peut-être un "intros H: <- H': [ | ]" ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de résoudre des buts comme celui-ci :
Record nat_retract : Type :=
{f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
Goal nat_retract.
exists (fun x => x) (fun x => x).
- Nouvelle tentative d'utilisation des types des metas/evars pour
inférer de nouvelles instances de metas/evars; permet par exemple
d'utiliser f_equal sans option with, mais aussi, avec la modif
précédente, de résoudre des buts tels que
Goal exists f:bool->Prop, f true = True.
exists (fun x => True).
[Les expériences passées avaient montré qu'en prenant en compte les
types dans l'unification, on peut unifier trop tôt une evars à une
mauvaise sorte; à défaut de mécanisme de prise en compte des problème
d'unification avec sous-typage, on s'est interdit ici d'unifier des
types qui sont des arités.]
- Tout les constr de tactic_expr deviennent des open_constr (même si seul
with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par sa notation (p.ex. pour unfold ou pour lazy delta).
Ex: Goal 3+4 = 7. unfold "+".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des
wit_tactic en types créés dynamiquement (révisions 8917 et 8926).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9393 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8973 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de
pouvoir typer correctement les wit_tactic (auparavant le typage des
wit_tactic était trop libéral et permettait de casser la
subject-reduction).
Amélioration au passage de l'affichage de la tactique "replace by"
(module Extratactics).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
|
