diff options
| author | letouzey | 2012-05-29 11:08:50 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:50 +0000 |
| commit | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (patch) | |
| tree | 44b4f39e7f92f29f4626d4aa8265fe68eb129111 /parsing/g_tactic.ml4 | |
| parent | a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (diff) | |
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4c1d747ea1..c373371d2f 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -13,7 +13,7 @@ open Util open Tacexpr open Genredexpr open Genarg -open Topconstr +open Constrexpr open Libnames open Termops open Tok @@ -129,7 +129,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = (* Functions overloaded by quotifier *) let induction_arg_of_constr (c,lbind as clbind) = if lbind = NoBindings then - try ElimOnIdent (constr_loc c,snd(coerce_to_id c)) + try ElimOnIdent (Topconstr.constr_loc c,snd(Topconstr.coerce_to_id c)) with _ -> ElimOnConstr clbind else ElimOnConstr clbind @@ -163,7 +163,7 @@ let rec mkCLambdaN_simple_loc loc bll c = let mkCLambdaN_simple bl c = if bl=[] then c else - let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in + let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Topconstr.constr_loc c) in mkCLambdaN_simple_loc loc bl c let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) |