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/funind/g_indfun.ml4 | |
| 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/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 2fdf62d26..ef2276134 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -368,7 +368,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list = an occurence of function [id] in the conclusion of goal [g]. If [id]=[None] then calls to any function are selected. In any case [heuristic] is used to select the most pertinent occurrence. *) -let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list) +let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) (nexttac:Proof_type.tactic) g = let test = match oid with | Some id -> @@ -468,10 +468,10 @@ VERNAC COMMAND EXTEND MergeFunind let ar2 = List.length (fst (decompose_prod f2type)) in let _ = if ar1 <> List.length cl1 then - Errors.error ("not the right number of arguments for " ^ string_of_id id1) in + Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in let _ = if ar2 <> List.length cl2 then - Errors.error ("not the right number of arguments for " ^ string_of_id id2) in + Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id ] END |