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 | |
| 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')
| -rw-r--r-- | tactics/auto.ml | 6 | ||||
| -rw-r--r-- | tactics/dhyp.ml | 2 | ||||
| -rw-r--r-- | tactics/pattern.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e1c4caad77..02d76010cc 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -330,7 +330,7 @@ let _ = vinterp_add "HintResolve" (function - | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] -> + | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] -> let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in let dbnames = if l = [] then ["core"] else List.map (function VARG_IDENTIFIER i -> string_of_id i @@ -342,7 +342,7 @@ let _ = vinterp_add "HintImmediate" (function - | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] -> + | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] -> let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in let dbnames = if l = [] then ["core"] else List.map (function VARG_IDENTIFIER i -> string_of_id i @@ -377,7 +377,7 @@ let _ = "HintExtern" (function | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; - VARG_NUMBER pri; VARG_COMMAND patcom; VARG_TACTIC tacexp] -> + VARG_NUMBER pri; VARG_CONSTR patcom; VARG_TACTIC tacexp] -> let pat = Pattern.raw_sopattern_of_compattern (Global.env()) patcom in let dbnames = if l = [] then ["core"] else diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 6efa9c686f..1b47b7c1e4 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -206,7 +206,7 @@ let add_destructor_hint na pat pri code = let _ = vinterp_add "HintDestruct" (function - | [VARG_IDENTIFIER na; VARG_AST location; VARG_COMMAND patcom; + | [VARG_IDENTIFIER na; VARG_AST location; VARG_CONSTR patcom; VARG_NUMBER pri; VARG_AST tacexp] -> let loc = match location with | Node(_,"CONCL",[]) -> Concl() 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 |