diff options
| author |  Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
| commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
| tree | dabcac548e299fee1da464c93b3dba98484f45b1 /proofs/proof_type.ml | |
| parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) | |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6f8b0686..dbe40780 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.ml 9573 2007-01-31 20:18:18Z notin $ *) +(*i $Id: proof_type.ml 9842 2007-05-20 17:44:23Z herbelin $ *) (*i*) open Environ @@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -73,7 +73,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -83,7 +83,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, |