diff options
author | 2009-09-17 15:58:14 +0000 | |
---|---|---|
committer | 2009-09-17 15:58:14 +0000 | |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /tactics/evar_tactics.ml | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/evar_tactics.ml')
-rw-r--r-- | tactics/evar_tactics.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 0d08b72aa..ad392c7d8 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -21,31 +21,31 @@ open Termops (* The instantiate tactic *) -let evar_list evc c = +let evar_list evc c = let rec evrec acc c = match kind_of_term c with | Evar (n, _) when Evd.mem evc n -> c :: acc | _ -> fold_constr evrec acc c - in + in evrec [] c -let instantiate n (ist,rawc) ido gl = +let instantiate n (ist,rawc) ido gl = let sigma = gl.sigma in - let evl = + let evl = match ido with - ConclLocation () -> evar_list sigma gl.it.evar_concl + ConclLocation () -> evar_list sigma gl.it.evar_concl | HypLocation (id,hloc) -> let decl = Environ.lookup_named_val id gl.it.evar_hyps in match hloc with - InHyp -> - (match decl with + InHyp -> + (match decl with (_,None,typ) -> evar_list sigma typ - | _ -> error + | _ -> error "Please be more specific: in type or value?") | InHypTypeOnly -> let (_, _, typ) = decl in evar_list sigma typ | InHypValueOnly -> - (match decl with + (match decl with (_,Some body,_) -> evar_list sigma body | _ -> error "Not a defined hypothesis.") in if List.length evl < n then @@ -59,9 +59,9 @@ let instantiate n (ist,rawc) ido gl = (tclEVARS sigma') tclNORMEVAR gl - + let let_evar name typ gls = let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) typ in Refiner.tclTHEN (Refiner.tclEVARS sigma') (Tactics.letin_tac None name evar None nowhere) gls - + |