diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 11:10:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 11:10:24 +0000 |
| commit | 29c67f1d97221755415ace1e4317cb7af92e24f3 (patch) | |
| tree | 3aaa1283625e248b31339dbb76279629ae27f02e /.depend.camlp4 | |
| parent | 5a5c8682bcf7041f5a240b565f68e37478414b81 (diff) | |
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.depend.camlp4')
| -rw-r--r-- | .depend.camlp4 | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/.depend.camlp4 b/.depend.camlp4 index 94a85c980..bbbdb186c 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -1,7 +1,22 @@ tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo +tactics/eqdecide.ml: parsing/grammar.cma +tactics/extraargs.ml: parsing/grammar.cma +tactics/extratactics.ml: parsing/grammar.cma +tactics/eauto.ml: parsing/grammar.cma +contrib/interface/debug_tac.ml: parsing/grammar.cma +contrib/interface/centaur.ml: parsing/grammar.cma contrib/correctness/psyntax.ml: parsing/grammar.cma +contrib/omega/g_omega.ml: parsing/grammar.cma +contrib/romega/g_romega.ml: parsing/grammar.cma +contrib/ring/g_quote.ml: parsing/grammar.cma +contrib/ring/g_ring.ml: parsing/grammar.cma contrib/field/field.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo +contrib/fourier/g_fourier.ml: parsing/grammar.cma +contrib/extraction/g_extraction.ml: parsing/grammar.cma +contrib/xml/xmlentries.ml: parsing/grammar.cma +contrib/jprover/jprover.ml: parsing/grammar.cma parsing/lexer.ml: +parsing/q_util.ml: parsing/q_coqast.ml: parsing/g_prim.ml: parsing/pcoq.ml: @@ -13,7 +28,8 @@ parsing/g_cases.ml: parsing/grammar.cma parsing/g_constr.ml: parsing/grammar.cma parsing/g_tactic.ml: parsing/grammar.cma parsing/g_ltac.ml: parsing/grammar.cma -parsing/extend.ml: parsing/grammar.cma +parsing/tacextend.ml: +parsing/vernacextend.ml: toplevel/mltop.ml: lib/pp.ml: contrib/xml/xml.ml: |