diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-02 13:06:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-02 13:06:14 +0000 |
| commit | 7003ff317ba1fce8898538801a1c8ecf1fddb972 (patch) | |
| tree | ca480ac6360f0204deb2f5ac1227d553e3ef3ff9 /tactics/hipattern.ml | |
| parent | 638d3095c34d230e025fc21567d725bd0616d9cf (diff) | |
Divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@397 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b8a004a58..ccc073b1a 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -22,7 +22,7 @@ open Pattern type module_mark = Stock.module_mark -let parse_constr s = +let parse_astconstr s = try Pcoq.parse_string Pcoq.Constr.constr_eoi s with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> @@ -30,8 +30,8 @@ let parse_constr s = (* Patterns *) let parse_pattern s = - Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_constr s) - + Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s) + type marked_pattern = (int list * constr_pattern) Stock.stocked let (pattern_stock : (int list * constr_pattern) Stock.stock) = @@ -44,7 +44,7 @@ let make_module_marker = Stock.make_module_marker (* Squeletons *) let parse_squeleton s = - let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s) in + let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_astconstr s) in (collect_metas c, c) type marked_term = (int list * constr) Stock.stocked |