diff options
| author | herbelin | 2006-03-22 08:27:14 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-22 08:27:14 +0000 |
| commit | 8fb0925c056c3e9a6103355eed31d283d6498070 (patch) | |
| tree | b41aa3abb75d4b3e89136e2573687bd3cf65603e /Makefile | |
| parent | dfa81d7860309029d100cd5348d2dd6bd8fa33c9 (diff) | |
- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de
la compilation de fichiers comme hipattern.ml (renommé en
hipattern.ml4)
- Extension de eqdecide.ml4 pour qu'il gère les buts sans
quantificateurs, basés soient sur sumbool soit sur or, et à symétrie
près de la disjunction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -208,7 +208,7 @@ HIGHTACTICS=\ SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4 USERTAC = $(SPECTAC) ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \ - tactics/eauto.ml4 toplevel/whelp.ml4 + tactics/eauto.ml4 toplevel/whelp.ml4 tactics/hipattern.ml4 USERTACCMO=$(USERTAC:.ml4=.cmo) USERTACCMX=$(USERTAC:.ml4=.cmx) @@ -1413,7 +1413,7 @@ ML4FILES +=parsing/g_minicoq.ml4 \ parsing/g_xml.ml4 parsing/g_constr.ml4 \ parsing/g_tactic.ml4 parsing/g_ltac.ml4 \ parsing/argextend.ml4 parsing/tacextend.ml4 \ - parsing/vernacextend.ml4 + parsing/vernacextend.ml4 parsing/q_constr.ml4 # beforedepend:: $(GRAMMARCMO) |