diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
| commit | 8030a420d2cfcf8372d5fe6544efbecde940381b (patch) | |
| tree | 6d4a3c198d4dbecf0cf15f3b53c31447aacfafd7 /proofs | |
| parent | faa2647739aa33421328af4ffeaba1bb474e868e (diff) | |
syntaxe AST Inversion + commentaires ocamlweb autour de $
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_trees.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 | ||||
| -rw-r--r-- | proofs/refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/stock.mli | 2 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 3 |
11 files changed, 13 insertions, 10 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index aaf9637f8..05baad0ca 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Util diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index ac6bc0630..169fde57b 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/logic.mli b/proofs/logic.mli index 1038b5c0d..8591e3367 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 0ea35bea9..8b8e41b34 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Pp diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index c2b73c85d..043e39170 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Util diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 1c1b66077..dbc4ba655 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Environ diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 68767dc8c..f35949580 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Term diff --git a/proofs/stock.mli b/proofs/stock.mli index c0cd43c7d..c08a5b480 100644 --- a/proofs/stock.mli +++ b/proofs/stock.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 800d89051..a23f953e6 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Dyn diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ee80beba8..a7cf3b6cc 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 26ab1a947..fffe58348 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -1,3 +1,6 @@ + +(*i $Id$ i*) + open Proof_type open Term |