diff options
| author | herbelin | 2001-01-24 22:26:14 +0000 |
|---|---|---|
| committer | herbelin | 2001-01-24 22:26:14 +0000 |
| commit | 161e0e8073e84ab0f3e982baf7f7122dd3ddfb85 (patch) | |
| tree | 83ef95a0f573d7777aa92221c00b662f199000ad /tactics/tactics.ml | |
| parent | 8b744c66b48182406ecc6d671312204c74c1a53f (diff) | |
Prise en compte des noms longs dans les Hints et les Coercions, et réorganisations diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 087821d7ab..1080b95092 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -221,15 +221,10 @@ let dyn_reduce = function (* Unfolding occurrences of a constant *) -let unfold_constr c = - match kind_of_term (strip_outer_cast c) with - | IsConst(sp,_) -> - unfold_in_concl [[],sp] - | IsVar(id) -> let sp = Lib.make_path id CCI in - unfold_in_concl [[],sp] - | _ -> - errorlabstrm "unfold_constr" - [< 'sTR "Cannot unfold a non-constant." >] +let unfold_constr = function + | ConstRef sp -> unfold_in_concl [[],sp] + | VarRef sp -> unfold_in_concl [[],sp] + | _ -> errorlabstrm "unfold_constr" [< 'sTR "Cannot unfold a non-constant.">] (*******************************************) (* Introduction tactics *) @@ -1718,9 +1713,9 @@ let abstract_subproof name tac gls = with e when catchable_exception e -> (delete_current_proof(); raise e) in (* Faudrait un peu fonctionnaliser cela *) - Declare.declare_constant na (ConstantEntry const,strength,true); + let sp = Declare.declare_constant na (ConstantEntry const,strength,true) in let newenv = Global.env() in - Declare.construct_reference newenv CCI na + Declare.constr_of_reference Evd.empty newenv (ConstRef sp) in exact_no_check (applist (lemme, List.map mkVar (List.rev (ids_of_named_context sign)))) |