diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-03-27 07:43:43 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-03-27 07:45:11 +0200 |
| commit | 6e34b272d789455a9be589e27ad3a998cf25496b (patch) | |
| tree | 57b74c7cbafd705a1ebce7d16cdaec02b704fb44 /plugins | |
| parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
| parent | 2bdcd093b357adb2185518dabbafd1a0b9279044 (diff) | |
Remove non-DFSG contentsupstream/8.3.pl4+dfsg
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/recdef.ml | 5 | ||||
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 4 |
3 files changed, 6 insertions, 5 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 83868da9..934bf683 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: recdef.ml 15069 2012-03-20 14:06:07Z herbelin $ *) open Term open Termops @@ -51,7 +51,8 @@ open Genarg let compute_renamed_type gls c = - rename_bound_vars_as_displayed [] (pf_type_of gls c) + rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] + (pf_type_of gls c) let qed () = Lemmas.save_named true let defined () = Lemmas.save_named false diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index c82abfc8..04eac3a8 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -872,7 +872,7 @@ Arguments Scope Tint [Int_scope]. Arguments Scope Tplus [romega_scope romega_scope]. Arguments Scope Tmult [romega_scope romega_scope]. Arguments Scope Tminus [romega_scope romega_scope]. -Arguments Scope Topp [romega_scope romega_scope]. +Arguments Scope Topp [romega_scope]. Infix "+" := Tplus : romega_scope. Infix "*" := Tmult : romega_scope. diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index d3a63410..80e712e5 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -485,8 +485,8 @@ and solve_obligation_by_tac prg obls i tac = true else false with - | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) - | Stdpp.Exc_located(_, Refiner.FailError (_, s)) + | Compat.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) + | Compat.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s) | e -> false |