diff options
| author | herbelin | 2000-01-07 22:27:11 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-07 22:27:11 +0000 |
| commit | 424bf8a5131aaf4960745c7050e5977c6e5fd4a5 (patch) | |
| tree | e23b22a6a106a7cbc0cd54cd48098f5c6aaceb68 /tactics/pattern.ml | |
| parent | f5863b8f5a6c8791f089a2ddb43978a298394c95 (diff) | |
Renommage command en constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/pattern.ml')
| -rw-r--r-- | tactics/pattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/pattern.ml b/tactics/pattern.ml index fc5b6a4466..3038933e9a 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -35,7 +35,7 @@ let raw_sopattern_of_compattern env com = let parse_pattern s = let com = try - Pcoq.parse_string Pcoq.Command.command_eoi s + Pcoq.parse_string Pcoq.Constr.constr_eoi s with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> error "Malformed pattern" in |