diff options
| author | herbelin | 2009-08-04 12:37:05 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-04 12:37:05 +0000 |
| commit | 0fec4583628dfba57c4bbcf10e8c1fc053c5ec93 (patch) | |
| tree | 18018c90d6c3587d1b5d65d4e57ae32f0ef500de /toplevel | |
| parent | a42d753ac38896e58158311b3c384e80c9fd3fd4 (diff) | |
- Add more precise error localisation when one of the application fails
in a chain of apply or apply-in.
- Improved comments on the notions of permutation used in the library (still
the equality relation in file Permutation.v misses the property of being
effectively an equivalence relation, hence missing expected properties of
this notion of permutation).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 66d02278c3..5ddf2b7055 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -535,7 +535,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) tclREPEAT ( tclTHENSEQ [ - apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None; + simple_apply_in freshz (andb_prop()); fun gl -> let fresht = fresh_id (!avoid) (id_of_string "Z") gsig in |