diff options
Diffstat (limited to 'pretyping')
68 files changed, 461 insertions, 327 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 8ac471404..84295959f 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index b499da3ab..65e3c3be5 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a0434f927..10e259209 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module CVars = Vars diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 43dbc3105..04a346467 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index e42576d95..7cfb30f4c 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 1d4c88ea2..2ac59911c 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 6d5ee504e..a0804b72b 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 47b41f17b..f8600bbe0 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7cfd2e27d..04cb6a59f 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Hugo Herbelin for Coq V7 by isolating the coercion diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index a8c07d2ef..6cfd958b4 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Evd diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index c3a221944..888c76e3d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index e4d9ff9e1..3c2c73915 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module implements pattern-matching on terms *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 18ecbf8ed..f98a3b0db 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module CVars = Vars diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index f150cb195..32b94e1b0 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index dc3acbc3e..0a63985bf 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index d793b06d3..627430708 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index fd83795f5..03f40ad92 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Sorts diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 869e3adbf..cd23f9c60 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index e6d1e59b3..c9030be2d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Sorts diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 703c4616c..9b21599b6 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index fd6bfe0a2..b16087031 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index e77d8ff64..9ba63b4f5 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Locus diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml index 768ef3cfd..1f8b92636 100644 --- a/pretyping/geninterp.ml +++ b/pretyping/geninterp.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli index ae0b26e59..fa522e9c3 100644 --- a/pretyping/geninterp.mli +++ b/pretyping/geninterp.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Interpretation functions for generic arguments and interpreted Ltac diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 25817478e..2280ee2d4 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 0d9fb1f45..124440f5d 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index b7b5b1662..3327c250d 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* File initially created by Christine Paulin, 1996 *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index a9838cffe..119ff5222 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 275a079d5..8e3c33ff7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -643,8 +645,9 @@ let type_of_projection_knowing_arg env sigma p c ty = (* A function which checks that a term well typed verifies both syntactic conditions *) -let control_only_guard env c = - let check_fix_cofix e c = match kind c with +let control_only_guard env sigma c = + let check_fix_cofix e c = + match kind (EConstr.to_constr sigma c) with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> @@ -653,6 +656,6 @@ let control_only_guard env c = in let rec iter env c = check_fix_cofix env c; - iter_constr_with_full_binders push_rel iter env c + iter_constr_with_full_binders sigma EConstr.push_rel iter env c in iter env c diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 55149552a..296f25d3f 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -198,4 +200,4 @@ val type_of_inductive_knowing_conclusion : env -> evar_map -> Inductive.mind_specif Univ.puniverses -> EConstr.types -> evar_map * EConstr.types (********************) -val control_only_guard : env -> types -> unit +val control_only_guard : env -> Evd.evar_map -> EConstr.types -> unit diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index a4097237f..20883f6f6 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Reduction diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli index a5037ea47..a0c8d339a 100644 --- a/pretyping/inferCumulativity.mli +++ b/pretyping/inferCumulativity.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 86bc47132..1664e68f2 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Locus diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index 718d074cf..a07c018c3 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index f0cb8fd1f..c5ce0496b 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index dae29208e..abe817fe5 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Misctypes diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index b41e15f5a..fcbf50fea 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors open Term diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 579a7d2ac..67b7a2a40 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 1bec4a6f1..3fab553cb 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 2d1ce1dbc..9f0878578 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 7149d62a1..278a4761d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 430755ea0..6f14d025c 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6700748eb..4bcb7e459 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This file contains the syntax-directed part of the type inference @@ -923,7 +925,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in - let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + let fsign = if Flags.version_strictly_greater Flags.V8_6 then Context.Rel.map (whd_betaiota !evdref) fsign else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = @@ -1036,7 +1038,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in let cs_args = - if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + if Flags.version_strictly_greater Flags.V8_6 then Context.Rel.map (whd_betaiota !evdref) cs_args else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = @@ -1205,8 +1207,7 @@ let all_no_fail_flags = default_inference_flags false let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in - let evd, f = Evarutil.nf_evars_and_universes evd in - f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd + c, Evd.evar_universe_context evd (** Entry points of the high-level type synthesis algorithm *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 864768fe5..415c4e172 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file implements type inference. It maps [glob_constr] @@ -12,7 +14,6 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) -open Constr open Environ open Evd open EConstr @@ -26,7 +27,7 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - ?loc:Loc.t -> env -> int list list -> rec_declaration -> int array + ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint @@ -85,9 +86,8 @@ val understand_ltac : inference_flags -> heuristics (but no external tactic solver hook), as well as to ensure that conversion problems are all solved and that no unresolved evar remains, expanding evars. *) - val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> - env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context + env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver diff --git a/pretyping/program.ml b/pretyping/program.ml index bdc34bc53..52d940d8e 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/pretyping/program.mli b/pretyping/program.mli index 70ab97e83..df0848ba1 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index ab1f3cd32..d070edead 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Amokrane Saïbi, Dec 1998 *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index f15418577..1f7b23c0c 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/redops.ml b/pretyping/redops.ml index b5e4a7acb..90c3bdfae 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Genredexpr diff --git a/pretyping/redops.mli b/pretyping/redops.mli index 435b25091..285931ecd 100644 --- a/pretyping/redops.mli +++ b/pretyping/redops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Genredexpr diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 418ea271c..e8b19f6bc 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -1484,16 +1486,12 @@ let hnf_lam_appvect env sigma t nl = let hnf_lam_applist env sigma t nl = List.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl -let bind_assum (na, t) = - (na, t) - let splay_prod env sigma = let rec decrec env m c = let t = whd_all env sigma c in match EConstr.kind sigma t with | Prod (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (bind_assum (n,a)::m) c0 + decrec (push_rel (LocalAssum (n,a)) env) ((n,a)::m) c0 | _ -> m,t in decrec env [] @@ -1503,8 +1501,7 @@ let splay_lam env sigma = let t = whd_all env sigma c in match EConstr.kind sigma t with | Lambda (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (bind_assum (n,a)::m) c0 + decrec (push_rel (LocalAssum (n,a)) env) ((n,a)::m) c0 | _ -> m,t in decrec env [] diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 0565baf45..3b56513f5 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -276,7 +278,7 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. - @raises UniverseInconsistency iff catch_incon is set to false, + @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 00b175c48..3582b6447 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 6fdde9046..40424ead4 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Evd diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9b9408698..518d2f604 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index a6b8262f7..aa7604f53 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 3f947fd23..08051fd3a 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index ee28ec173..b80c28711 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -93,7 +95,12 @@ val no_goals : evar_filter val no_goals_or_obligations : evar_filter (** Resolvability. - Only undefined evars can be marked or checked for resolvability. *) + Only undefined evars can be marked or checked for resolvability. + They represent type-class search roots. + + A resolvable evar is an evar the type-class engine may try to solve + An unresolvable evar is an evar the type-class engine will NOT try to solve +*) val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t val is_resolvable : evar_info -> bool diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index dc8ff2e20..6475388f9 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 557aa3c9f..ce647029f 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Loc diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 3cc152017..542bf775f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module CVars = Vars diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 153a48a71..fe83a2cc8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e1720ec95..f4269a2c5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -193,7 +195,7 @@ let pose_all_metas_as_evars env evd t = let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in let ty = - if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + if Flags.version_strictly_greater Flags.V8_6 then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in @@ -248,20 +250,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -let global_pattern_unification_flag = ref true - -open Goptions - -(* Compatibility option introduced and activated in Coq 8.4 *) - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "pattern-unification for existential variables in tactics"; - optkey = ["Tactic";"Pattern";"Unification"]; - optread = (fun () -> !global_pattern_unification_flag); - optwrite = (:=) global_pattern_unification_flag } - type core_unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; (* What this flag controls was activated with all constants transparent, *) @@ -285,12 +273,10 @@ type core_unify_flags = { use_pattern_unification : bool; (* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *) - (* This says if pattern unification is tried; can be overwritten with *) - (* option "Set Tactic Pattern Unification" *) + (* This says if pattern unification is tried *) use_meta_bound_pattern_unification : bool; - (* This is implied by use_pattern_unification (though deactivated *) - (* by unsetting Tactic Pattern Unification); has no particular *) + (* This is implied by use_pattern_unification; has no particular *) (* reasons to be set differently than use_pattern_unification *) (* except for compatibility of "auto". *) (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *) @@ -471,10 +457,10 @@ let set_flags_for_type flags = { flags with } let use_evars_pattern_unification flags = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification let use_metas_pattern_unification sigma flags nb l = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification || flags.use_meta_bound_pattern_unification && Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l @@ -1304,12 +1290,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - if Flags.version_less_or_equal Flags.V8_5 then - (* We used to force solving unrelated problems at arbitrary times *) - Evarconv.solve_unif_constraints_with_heuristics env evd - else (* solve_simple_eqn calls reconsider_unif_constraints itself *) - evd + | Success evd -> evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 085e8c5b8..16ce5c93d 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index 89f1185a9..d16f046fa 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli index 706d3a157..305d045b1 100644 --- a/pretyping/univdecls.mli +++ b/pretyping/univdecls.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Local universe and constraint declarations. *) @@ -12,8 +14,8 @@ type universe_decl = val default_univ_decl : universe_decl -val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> +val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr -> Evd.evar_map * universe_decl -val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> +val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> Evd.evar_map * universe_decl diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c93b41786..3c9b8bc33 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -141,7 +143,6 @@ and nf_vtype env sigma v = nf_val env sigma v crazy_type and nf_whd env sigma whd typ = match whd with - | Vsort s -> mkSort s | Vprod p -> let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in @@ -182,7 +183,8 @@ and nf_whd env sigma whd typ = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) in nf_univ_args ~nb_univs mk env sigma stk - | Vatom_stk(Atype u, stk) -> assert false + | Vatom_stk(Asort s, stk) -> + assert (List.is_empty stk); mkSort s | Vuniv_level lvl -> assert false @@ -200,7 +202,26 @@ and nf_univ_args ~nb_univs mk env sigma stk = let (t,ty) = mk u in nf_stk ~from:nb_univs env sigma t ty stk -and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = +and nf_evar env sigma evk stk = + let evi = try Evd.find sigma evk with Not_found -> assert false in + let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in + let concl = Evd.evar_concl evi in + if List.is_empty hyps then + nf_stk env sigma (mkEvar (evk, [||])) concl stk + else match stk with + | Zapp args :: stk -> + (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that + really an invariant? *) + let fold accu d = Term.mkNamedProd_or_LetIn d accu in + let t = List.fold_left fold concl hyps in + let t, args = nf_args env sigma args t in + let inst, args = Array.chop (List.length hyps) args in + let c = mkApp (mkEvar (evk, inst), args) in + nf_stk env sigma c t stk + | _ -> + CErrors.anomaly (Pp.str "Argument size mismatch when decompiling an evar") + +and constr_type_of_idkey env sigma (idkey : Vmvalues.id_key) stk = match idkey with | ConstKey cst -> let cbody = Environ.lookup_constant cst env in @@ -218,6 +239,8 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = let n = (nb_rel env - i) in let ty = RelDecl.get_type (lookup_rel n env) in nf_stk env sigma (mkRel n) (lift n ty) stk + | EvarKey evk -> + nf_evar env sigma evk stk and nf_stk ?from:(from=0) env sigma c t stk = match stk with @@ -355,8 +378,8 @@ and nf_cofix env sigma cf = mkCoFix (init,(name,cft,cfb)) let cbv_vm env sigma c t = - if Termops.occur_meta_or_existential sigma c then - CErrors.user_err Pp.(str "vm_compute does not support existential variables."); + if Termops.occur_meta sigma c then + CErrors.user_err Pp.(str "vm_compute does not support metas."); (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr sigma c in let t = EConstr.to_constr sigma t in diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index d1a996a34..3e0eabb01 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr |