diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 2 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 8 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 6 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 2 |
6 files changed, 11 insertions, 11 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 97ea5fdc..bc3d9ed5 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 0dcf3a87..b73c8eef 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -20,8 +20,8 @@ type pa_fun= fnargs:int} -module PafMap : Map.S with type key = pa_fun -module PacMap : Map.S with type key = pa_constructor +module PafMap : CSig.MapS with type key = pa_fun +module PacMap : CSig.MapS with type key = pa_constructor type cinfo = {ci_constr: pconstructor; (* inductive type *) @@ -185,7 +185,7 @@ val empty_forest: unit -> forest (*type pa_constructor -module PacMap:Map.S with type key=pa_constructor +module PacMap:CSig.MapS with type key=pa_constructor type term = Symb of Term.constr diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 42c03234..c188bf3b 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 2ff2bd38..eacbfeac 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 068cb25c..0baa5337 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -501,9 +501,9 @@ let f_equal = let concl = Proofview.Goal.concl gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) - Tacticals.New.tclTHEN + Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) - (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)) + [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)] with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index aa31c6f0..5dbc340c 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |