Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 27 lines (20 sloc) 1.095 kB
d6c87f2 New script dev/tools/change-header to automatically update Coq files …
herbelin authored
1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
a234672 Updating headers.
herbelin authored
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
d6c87f2 New script dev/tools/change-header to automatically update Coq files …
herbelin authored
4 (* \VV/ **************************************************************)
5 (* // * This file is distributed under the terms of the *)
6 (* * GNU Lesser General Public License Version 2.1 *)
7 (************************************************************************)
37c82d5 Prise en compte des coercions dans les clauses "with" même si le type
herbelin authored
8
9 open Names
10 open Term
11 open Environ
12
13 (** This module is about the computation of an approximation of the
14 head symbol of defined constants and local definitions; it
15 provides the function to compute the head symbols and a table to
16 store the heads *)
17
f73d7c4 @pirbo Move from ocamlweb to ocamdoc to generate mli documentation
pirbo authored
18 (** [declared_head] computes and registers the head symbol of a
37c82d5 Prise en compte des coercions dans les clauses "with" même si le type
herbelin authored
19 possibly evaluable constant or variable *)
20
21 val declare_head : evaluable_global_reference -> unit
22
f73d7c4 @pirbo Move from ocamlweb to ocamdoc to generate mli documentation
pirbo authored
23 (** [is_rigid] tells if some term is known to ultimately reduce to a term
37c82d5 Prise en compte des coercions dans les clauses "with" même si le type
herbelin authored
24 with a rigid head symbol *)
25
26 val is_rigid : env -> constr -> bool
Something went wrong with that request. Please try again.