diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /plugins/firstorder | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/formula.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/ground.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/instances.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/rules.mli | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index d224f87df..093087511 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -116,7 +116,7 @@ type side = Hyp | Concl | Hint let no_atoms = (false,{positive=[];negative=[]}) -let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *) +let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *) let build_atoms gl metagen side cciterm = let trivial =ref false diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 753fdda72..48e60d798 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -25,7 +25,7 @@ let update_flags ()= red_flags:= Closure.RedFlags.red_add_transparent Closure.betaiotazeta - (Names.Idpred.full,Names.Cpred.complement !predref) + (Names.Id.Pred.full,Names.Cpred.complement !predref) let ground_tac solver startseq gl= update_flags (); diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 414afad46..c7a582a0e 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -98,7 +98,7 @@ let rec collect_quantified seq= let dummy_constr=mkMeta (-1) -let dummy_bvid=id_of_string "x" +let dummy_bvid=Id.of_string "x" let mk_open_instance id gl m t= let env=pf_env gl in diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 78a70ff51..bfebbaaf8 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -19,7 +19,7 @@ type 'a with_backtracking = tactic -> 'a val wrap : int -> bool -> seqtac -val basename_of_global: global_reference -> identifier +val basename_of_global: global_reference -> Id.t val clear_global: global_reference -> tactic |